Au temps en emporte le C

Steven de Oliveira 1 Virgile Prévosto 1 Sébastien Bardin 1
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Résumé : Le (bon) séquencement des événements au fil du temps fait partie des nombreux sujets d'analyse de programmes, par exemple pour l'étude de protocoles d'échange d'information ou de systèmes embarqués. De nombreux travaux de logique temporelle linéaire (LTL) permettent de décrire formellement le comportement attendu d'un programme, sous la forme d'une succession d’actions distinctes. Implanté au sein de Frama-C, plate-forme d'analyse de code source en langage C, le greffon Aoraï permet la génération de spécifications équivalentes, dans leur ensemble, à la conformité d'un programme C donné vis à vis d'une formule de logique temporelle linéaire. Ce greffon discrétise le temps de telle sorte que seuls les appels et les retours de fonctions sont considérés comme des événements. Cet article présente Model-CaRet, un nouveau greffon Frama-C qui généralise la trace étudiée par Aoraï. Plus précisément, Model-CaRet est dédié à la génération du test de satisfiabilité, et à sa vérification automatique, d'une formule de logique CaRet sur un programme C, représenté sous la forme d'une machine à états récursif. CaRet est une extension naturelle de la LTL permettant l'étude simultanée de plusieurs traces d'exécution, et en particulier de manipuler explicitement la pile d'appel du programme dans les formules.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099128
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:23:58 PM
Last modification on : Thursday, February 7, 2019 - 2:22:55 PM
Long-term archiving on : Wednesday, April 1, 2015 - 10:11:20 AM

File

jfla15_submission_12.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099128, version 1

Citation

Steven de Oliveira, Virgile Prévosto, Sébastien Bardin. Au temps en emporte le C. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099128⟩

Share

Metrics

Record views

174

Files downloads

237