An Approach for Verifying Concurrent C Programs
| 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), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), 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), Methni, Amira |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: | |
| Zdroj: | Proceedings of 8th Junior Researcher Workshop on Real-Time Computing 8th Junior Researcher Workshop on Real-Time Computing 8th Junior Researcher Workshop on Real-Time Computing, Oct 2014, Versailles, France. pp.33-36 |
| Popis: | International audience; As software system and its complexity are fast growing, software correctness becomes more and more a crucial issue. We address the problem of verifying functional properties of real-time operating system (microkernel) implemented with C. We present a work-in-progress approach for formally specifying and verifying concurrent C programs directly based on the semantics of C. The basis of this approach is to automatically translate a C code into a TLA+ specification which can be checked by the TLC model checker. We define a set of translation rules and implement it in a tool (C2TLA+) that automatically translates C code into a TLA+ specification. Generated specifications can be integrated with manually written specifications that provide primitives that cannot be expressed in C, or that provide abstract versions of the generated specifications to address the state-explosion problem. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|