Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs

P. Baudin , D. Delmas (1) , S Duprat (2) , B Monate

1 Airbus [France]
2 ATOS Origin

More and more control/command software is being generated automatically from high­level graphical specifications. Such specifications are typically synchronous data­flow models, built on a set of external basic operators to be implemented in a lower­level language. The semantics of the overall model depends therefore on the semantics of the basic operators, which can be expressed in terms of temporal (inductive multi­cycle) definitions. In this paper, we describe a way to specify and verify these operator formally, using theorem­proving techniques. We report on experiments conducted to prove multi­cycle properties on actual embedded basic operators written in C, using the CAVEAT static analyser with a dedicated method.

Keywords: formal verification; theoremproving; static analysis; CAVEAT; embedded software

Domains: Computer Science [cs]; Embedded Systems

P. Baudin, D. Delmas, S Duprat, B Monate. Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs. 4th International Congress ERTS 2008, Jan 2008, Toulouse, France. ⟨insu-02269744⟩