Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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.
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.laas.fr/hal-01949464
Contributor : Silvano Dal Zilio <>
Submitted on : Monday, December 10, 2018 - 10:36:39 AM
Last modification on : Thursday, June 10, 2021 - 3:02:00 AM
Long-term archiving on: : Monday, March 11, 2019 - 1:42:06 PM

File

autoflight-control-issre14.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

124

Files downloads

185