TY - GEN
T1 - Architecture-based design
T2 - 13th International Conference on Formal Aspects of Component Software, FACS 2016
AU - Mavridou, Anastasia
AU - Stachtiari, Emmanouela
AU - Bliudze, Simon
AU - Ivanov, Anton
AU - Katsaros, Panagiotis
AU - Sifakis, Joseph
N1 - Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - 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. We illustrate the following three steps of the design approach: (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 DFinder from the BIP tool-set. 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 by the model.
AB - 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. We illustrate the following three steps of the design approach: (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 DFinder from the BIP tool-set. 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 by the model.
U2 - 10.1007/978-3-319-57666-4_16
DO - 10.1007/978-3-319-57666-4_16
M3 - Conference contribution
AN - SCOPUS:85018345605
SN - 9783319576657
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 260
EP - 279
BT - Formal Aspects of Component Software - 13th International Conference, FACS 2016, Revised Selected Papers
A2 - Khosravi, Ramtin
A2 - Kouchnarenko, Olga
PB - Springer Verlag
Y2 - 19 October 2016 through 21 October 2016
ER -