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

International audienceMore 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