|
 
|
[MLH15] Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs
Conférence Internationale avec comité de lecture : The Tenth International Conference on Software Engineering Advances - ICSEA 2015 : , November 2015, pp.56-61, Barcelone, Spain,Mots clés: Temporal Logic of Actions; formal specification; model-checking; C programs; refinement mapping
Résumé:
One approach to verify the correctness of a system is to prove that it implements an executable (specification) model whose correctness is more obvious. Here we define a kind of automata whose state is the product of values of multiple variables that we name State Transition Systems (STS for short). We define the semantics of TLA+ constructs using STSs, in particular the notions of TLA+ models, data hiding, and implication between models. We implement these concepts and prove their usefulness by applying them to the verification of C programs against abstract (TLA+ or STS) models and properties.
Equipe:
sys
Collaboration:
CEA-LIST/LASTRE
BibTeX
| @inproceedings { | |||
| MLH15, | |||
| title | = | "{Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs}", | |
| author | = | " A. Methni and M. Lemerre and S. Haddad and K. Barkaoui and B. Ben Hedia ", | |
| booktitle | = | "{The Tenth International Conference on Software Engineering Advances - ICSEA 2015 : }", | |
| year | = | 2015, | |
| edition | = | "IARIA", | |
| month | = | "November", | |
| pages | = | "56-61", | |
| address | = | "Barcelone, Spain", | |
| } | |||
