title: Developing Mode-Rich Satellite Software by Refinement in Event-B
creator: Iliasov, Alexei
creator: Troubitsyna, Elena
creator: Laibinis, Linas
creator: Romanovsky, Alexander
creator: Varpaaniemi, Kimmo
creator: Ilic, Dubravka
creator: Latvala, Timo
subject: Event-B
subject: Industrial Deployment
subject: Methodology
description: One of the guarantees that the designers of on-board satellite systems need to provide, so as to ensure their dependability, is that the mode transition scheme is implemented correctly, i.e. that the states of system components are consistent with the global system mode. There is still, however, a lack of scalable approaches to developing and verifying systems with complex mode transitions. This paper presents an approach to formal development of mode-rich systems by refinement in Event-B. We formalise the concepts of modes and mode transitions as well as deriving specification and refinement patterns which support correct-by-construction system development. The proposed approach is validated by a formal development of the Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. The experience gained in the course of developing of as complex an industrial-size system as AOCS shows that refinement in Event-B provides the engineers with a scalable formal technique that enables both mode-rich systems development and proof-based verification of their mode consistency.
publisher: Elsevier
date: 2012
type: Article
type: PeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/386/1/FMICS_journal%2B-.pdf
identifier:   Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo  (2012) Developing Mode-Rich Satellite Software by Refinement in Event-B.  Science of Computer Programming. Accepted. In press .       (In Press)  
relation: http://deploy-eprints.ecs.soton.ac.uk/386/