|
 
|
[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éciï¬cation 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 aï¬n qu’il soit vériï¬Ã© 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éciï¬cation TLA+.
Equipe:
sys
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", | |
| } | |||
