WP2: Temporal Properties

Many properties that one wishes to verify in embedded software include some kind of temporal aspect. This stems from the fact that embedded software are often structured as reactive programs, i.e. as one global infinite loop defining a cyclic behaviour and reacting to sensors inputs. For example control/command programs have such a structure. Such code may be partially generated from high level specifications. To tackle cyclic behaviours of programs we propose to extend the ANSI/ISO C Specification Language (ACSL) with temporal operators like the pre operator of Lustre. Then we will propose techniques to perform static analysis geared toward verifying this new kind of properties.

This work package is connected with WP3 (Combining Static Analysis Techniques) and WP6 (Spreading Static Analysis). In addition, temporal properties are very often present in Scade specifications that are to be investigated formally in WP5 (Trusting Formal Methods), so that this item of WP5 strongly depends on WP2.