Attitude & Orbit Control System (AOCS) refers to a wider class of control systems which are used to determine and control the attitude of the spacecraft while in orbit, based on the information obtained from various sensors. In this paper, the authors propose an approach to evaluate a typical (yet somewhat simplified) AOCS architecture using formal development - based on the Event-B method. As a starting point, an Ada specification of the AOCS is translated into a formal specification and further refined to incorporate all the details of its original source code specification. This way the authors are able not only to evaluate the Ada specification by expressing and verifying specific system properties in our formal models, but also to determine how well the chosen modelling framework copes with the level of detail required for an actual implementation and code generation from the derived models.
Evaluating a control system architecture based on a formally derived AOCS model
Evaluation einer Steuerungssystemarchitektur basierend auf einem formal abgeleitetem AOCS-Modell
2010
6 Seiten, 3 Bilder, 3 Tabellen, 7 Quellen
(nicht paginiert)
Aufsatz (Konferenz)
Datenträger
Englisch
Evaluating a Control System Architecture Based on a Formally Derived AOCS Model
British Library Conference Proceedings | 2010
|Software safety architecture that can be formally verified
Kraftfahrwesen | 2004
|SLUB | 1994
A REUSABLE SOFTWARE ARCHITECTURE FOR SMALL SATELLITE AOCS SYSTEMS
British Library Conference Proceedings | 2006
|