Architecture-based Design: A Satellite On-board Software Case Study

In this case study, we apply the architecture-based design approach to the control software of the CubETH satellite. Architectures are a means for ensuring global coordination properties and thus, achieving correctness of complex systems by construction. The design approach comprises three main steps: 1) definition of a domain-specific taxonomy of architecture styles; 2) design of the software model by applying architectures to enforce the required properties; 3) deadlock-freedom analysis of the resulting model. We provide a taxonomy of architecture styles for satellite on-board software, formally defined by architecture diagrams in the BIP component-based framework. We show how architectures are instantiated from the diagrams and applied to a set of atomic components. Deadlock-freedom of the resulting model is verified using the DFinder tool from the BIP tool-set. Finally, we provide additional validation of our approach by using the nuXmv model checker to verify that the properties enforced by the architectures are, indeed, satisfied in the resulting software model.

Kouchnarenko, Olga
Khosravi, Ramtin
Published in:
Proceedings of the 13th International Conference on Formal Aspects of Component Software, 260--279
Presented at:
13th International Conference on Formal Aspects of Component Software (FACS 2016), Besançon, France, October 19-21, 2016

 Record created 2016-09-12, last modified 2018-09-13

BIP models:
Download fulltextZIP
NuXmv models:
Download fulltextZIP
Download fulltextPDF
Rate this document:

Rate this document:
(Not yet reviewed)