Rechercher

[MBB13] Traduction automatique du code C vers TLA+

Conférence Nationale avec comité de lecture : Ecole temps réel, August 2013, pp.pp.12-16, France,
motcle:
Résumé: Nous nous intéressons dans ce papier à l’automatisation de la traduction d’un code source C vers un modèle écrit dans le langage de spécification TLA+. Nous proposons alors un outil C2TLA+ pour automatiser le passage d’un code source C vers un modèle écrit dans un langage combinant une logique temporelle avec une logique des actions afin qu’il soit vérifié par le model-cheker TLC. Ce papier illustre les règles de représentation et de traduction utilisées pour passer d’une implémentation à une spécification TLA+.

Equipe: vespa
Collaboration: CEA-LIST/LASTRE

BibTeX

@inproceedings {
MBB13,
title="{Traduction automatique du code C vers TLA+}",
author=" A. Methni and K. Barkaoui and B. Ben Hedia and S. Haddad and M. Lemerre ",
booktitle="{Ecole temps réel}",
year=2013,
month="August",
pages="pp.12-16",
address=" France",
}