Proving Properties of Reactive Programs From C to Lustre

B. Blanc (1) , Loïc Correnson (1) , Zaynah Lea Dargaye (1) , J. Gassino (2) , B. Marre (1)

1 LIST (CEA) - Laboratoire d'Intégration des Systèmes et des Technologies
2 IRSN - Institut de Radioprotection et de Sûreté Nucléaire

In critical embedded software, proving functional properties of programs is a major area where formal methods are applied with an increasing success. Anyway, the more a property is complex, the more a high-level formal model of the software and its environment is required. However, in an industrial setting, such a model is not always available, or cannot be used for independent verification. We propose here a new route, where a high-level Lustre model is extracted from a C source program. Thus, high-level functional properties can be specified in Lustre and proved on this extracted model, hence on the real code, without requiring any additional formal documentation.

Mots clés: Formal Methods; Functional and Temporal Properties; Lustre; Scade; Embedded C; Reactive Programs

Domaines: Systèmes embarqués

B. Blanc, Loïc Correnson, Zaynah Lea Dargaye, J. Gassino, B. Marre. Proving Properties of Reactive Programs From C to Lustre. ERTS 2018 - 9th European Congress on Embedded Real Time Software and Systems, Jan 2018, Toulouse, France. ⟨hal-01708934⟩