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.


Editor(s):
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
Year:
2016
Publisher:
Springer
Keywords:
Laboratories:




 Record created 2016-09-12, last modified 2018-03-17

BIP models:
Download fulltextZIP
NuXmv models:
Download fulltextZIP
n/a:
Download fulltextPDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)