Formal Safety and Security Assessment of an Avionic Architecture with Alloy

Julien Brunel
(ONERA, Toulouse, France)
Laurent Rioux
(Thales Research & Technology)
Stéphane Paul
(Thales Research & Technology)
Anthony Faucogney
(All4Tec)
Frédérique Vallée
(All4Tec)

We propose an approach based on Alloy to formally model and assess a system architecture with respect to safety and security requirements. We illustrate this approach by considering as a case study an avionic system developed by Thales, which provides guidance to aircraft. We show how to define in Alloy a metamodel of avionic architectures with a focus on failure propagations. We then express the specific architecture of the case study in Alloy. Finally, we express and check properties that refer to the robustness of the architecture to failures and attacks.

In Jun Pang and Yang Liu: Proceedings Third International Workshop on Engineering Safety and Security Systems (ESSS 2014), Singapore, Singapore, 13 May 2014, Electronic Proceedings in Theoretical Computer Science 150, pp. 8–19.
Published: 3rd May 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.150.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org