Rechercher

[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: vespa
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",
}