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

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.