Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs - Archive ouverte HAL Access content directly
Conference Papers Year : 2008

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

, (1) , (2) ,
1
2
P. Baudin
  • Function : Author
D. Delmas
  • Function : Author
S Duprat
  • Function : Author
B Monate
  • Function : Author

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.
Fichier principal
Vignette du fichier
ERTS2008_0005_paper.pdf (809.49 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

insu-02269744 , version 1 (23-08-2019)

Identifiers

  • HAL Id : insu-02269744 , version 1

Cite

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⟩

Collections

INSU ERTS2008
27 View
9 Download

Share

Gmail Facebook Twitter LinkedIn More