HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download

Contributor : Axelle Pagnier Connect in order to contact the contributor
Submitted on : Friday, August 23, 2019 - 11:16:29 AM
Last modification on : Thursday, March 5, 2020 - 3:18:45 PM
Long-term archiving on: : Friday, January 10, 2020 - 6:41:39 AM


Files produced by the author(s)


  • HAL Id : insu-02269744, version 1



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⟩



Record views


Files downloads