Proving Temporal Properties at Code Level for Basic Operators of Control/Command Programs - INSU - Institut national des sciences de l'Univers Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

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

P. Baudin
  • Fonction : Auteur
D. Delmas
  • Fonction : Auteur
S Duprat
  • Fonction : Auteur
B Monate
  • Fonction : Auteur

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : insu-02269744 , version 1

Citer

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 Consultations
9 Téléchargements

Partager

Gmail Facebook X LinkedIn More