C2TLA+ : Traduction automatique du code C vers TLA+
| Autor: | Methni, Amira, Lemerre, Matthieu, Ben Hedia, Belgacem, Barkaoui, Kamel, Haddad, Serge |
|---|---|
| Přispěvatelé: | Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Methni, Amira |
| Jazyk: | francouzština |
| Rok vydání: | 2013 |
| Předmět: |
Model checking
TLA+ vérification formelle Model checking logique temporelle programmes C TLA+ [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] logique temporelle programmes C [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] vérification formelle |
| Zdroj: | École d’Été Temps Réel 2013 École d’Été Temps Réel 2013, Aug 2013, Toulouse, France |
| Popis: | National audience; 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-checker 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+. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|