[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)

Auteurs: A. Methni , K. Barkaoui , M. Lemerre , S. Haddad , B. Ben Hedia

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: sys

Collaboration: CEA-LIST/LASTRE

Download

BibTeX

@inproceedings {
	MBL15,
	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}",
	year	=	2015,
	edition	=	"Springer",
	month	=	"April",
	series	=	"Communications in Computer and Information Science",
	volume	=	476,
	pages	=	"206-222",
	address	=	" Luxembourg",
	doi	=	"10.1007/978-3-319-17581-2_14",
}