Model-Checking Real-Time Properties of an Auto Flight Control System Function

Pierre-Alain Bourdil (1) , Bernard Berthomieu (1) , Éric Jenn (2)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
2 Thales Avionics

We relate an experiment in modeling and verification of a part of an avionic function. The problem addressed is the correctness of a temporal condition enabling the detection of a range of faults in the implementation of the function. Using the Fiacre/Tina verification toolset, we produced a formal model abstracting the function, and confirmed by model-checking that the condition determined analytically is indeed correct. The modelling issues ensuring tractability of the model are discussed.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Pierre-Alain Bourdil, Bernard Berthomieu, Éric Jenn. Model-Checking Real-Time Properties of an Auto Flight Control System Function. IEEE International Symposium on Software Reliability Engineering, Nov 2014, Naples, Italy. ⟨10.1109/ISSREW.2014.40⟩. ⟨hal-01949464⟩