[MBL15] Specifying and Verifying Concurrent C Programs with TLA+

Conférence Internationale avec comité de lecture : Formal Techniques for Safety-Critical Systems, April 2015, Vol. 476, pp.206-222, Series Communications in Computer and Information Science, Luxembourg, (DOI: 10.1007/978-3-319-17581-2_14)

Mots clés: Concurrent C Programs, TLA+

Résumé: Verifying software systems automatically from their source code rather than modelling them in a dedicated language gives more confidence in establishing their properties. Here we propose a formal specification and verification approach for concurrent C programs directly based on the semantics of C. We define a set of translation rules and implement it in a tool (C2TLA+) that automatically translates C code into a TLA+ specification. The TLC model checker can use this specification to generate a model, allowing to check the absence of runtime errors and dead code in the C program in a given configuration. In addition, we show how translated specifications interact with manually written ones to: check the C code against safety or liveness properties; provide concurrency primitives or model hardware that cannot be expressed in C; and use abstract versions of translated C functions to address the state explosion problem. All these verifications have been conducted on an industrial case study, which is a part of the microkernel of the PharOS real-time system.

Equipe: vespa
Collaboration: CEA-LIST/LASTRE


@inproceedings {
title="{Specifying and Verifying Concurrent C Programs with TLA+}",
author=" A. Methni and K. Barkaoui and M. Lemerre and S. Haddad and B. Ben Hedia ",
booktitle="{Formal Techniques for Safety-Critical Systems}",
series="Communications in Computer and Information Science",
address=" Luxembourg",