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 metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal-insu.archives-ouvertes.fr/insu-02269744
Contributor : Axelle Pagnier <>
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

File

ERTS2008_0005_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : insu-02269744, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

33

Files downloads

15