Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Architecture-based Design: A Satellite On-board Software Case Study
 
conference paper

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

Mavridou, Anastasia  
•
Stachtiari, Emmanouela
•
Bliudze, Simon  
Show more
Kouchnarenko, Olga
•
Khosravi, Ramtin
2016
Proceedings of the 13th International Conference on Formal Aspects of Component Software
13th International Conference on Formal Aspects of Component Software (FACS 2016)

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

CubETH-BIPmodel.zip

Access type

openaccess

Size

18.63 KB

Format

ZIP

Checksum (MD5)

ed3a7b294f48ad1dc3ffbebe458b0fc7

Loading...
Thumbnail Image
Name

CubETH-SMVmodel.zip

Access type

openaccess

Size

31.37 KB

Format

ZIP

Checksum (MD5)

8e2aae01a6a96461eaadf4765ac9b709

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés