Home // ICSEA 2015, The Tenth International Conference on Software Engineering Advances // View article

Verifying and Constructing Abstract TLA Specifications: Application to the Verification of C programs

Authors:
Amira Methni
Matthieu Lemerre
Belgacem Ben Hedia
Serge Haddad
Kamel Barkaoui

Keywords: Temporal Logic of Actions; formal specification; model-checking; C programs; refinement mapping

Abstract:
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 System (STS). We define the semantics of TLA+ (specification language of the Temporal Logic of Actions) 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.

Pages: 56 to 61

Copyright: Copyright (c) IARIA, 2015

Publication date: November 15, 2015

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-438-1

Location: Barcelona, Spain

Dates: from November 15, 2015 to November 20, 2015