Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy

Julien Brunel , David Chemouil (1) , Vincent Ibanez , Nicolas Meledo

1 ONERA - The French Aerospace Lab [Toulouse]

We propose an approach based on Alloy to formally model and assess a system architecture with respect to system-level safety requirements. The system on which we instantiate our approach is a specific Required Navigation Performance system from a Thalès Avionics named Localizer Performance with Vertical guidance Approach (LPV). In this article, we describe how to define such a system architecture and how to verify safety objectives.

Keywords: Formal Modelling; Safety; Alloy

Domains: Computer Science [cs]; Computer Science [cs]; Embedded Systems

Julien Brunel, David Chemouil, Vincent Ibanez, Nicolas Meledo. Formal Modelling and Safety Analysis of an Avionic Functional Architecture with Alloy. Embedded real-time software and systems (ERTS² 2014), Feb 2014, TOULOUSE, France. ⟨hal-02272135⟩