Model Checking C Programs using OPEN/CAESAR

Organisation:	GISUM, University of Málaga (SPAIN)
Functionality:	Software Model Checking
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2006-2008
Description:	Model checking was initially proposed as a verification technique for systems described in high-level languages with a precise mathematical semantics, such as the Formal Description Techniques (FDTs) dedicated to concurrent systems. During the last years, the research community focused on extending the techniques and algorithms developed for FDTs in order to analyze programs written in usual algorithmic languages, such as C and Java. There are basically two methods for addressing this software model checking problem. The first one, based on model extraction, consists of translating the program into a particular FDT that is the input of an existing model checker. This allows to reuse the target tool, but requires the effort of constructing a high-level model of the original system. The second method consists in implementing new tools dedicated to specific programming languages. Although in general this may involve a considerable amount of development work, certain existing frameworks, such as the OPEN/CAESAR environment of CADP, can facilitate this task. OPEN/CAESAR allows a language to benefit from a whole range of on-the-fly verification tools, provided that the language is equipped with a compiler able to translate programs into their underlying Labelled Transition Systems (LTSs) represented in compliance with the interface defined by OPEN/CAESAR. In addition, OPEN/CAESAR provides various libraries implementing data structures (tables, stacks, hash functions, etc.) facilitating the development of LTS exploration algorithms. This work is a first step towards constructing an OPEN/CAESAR-compliant compiler for the C language. Currently, the C programs considered as input are client-server applications communicating via sockets. For these programs, the construction of an LTS according to the OPEN/CAESAR interface consists of three phases: Analyzing the C code. This phase is not trivial, because of the complexity of the C code. For simplicity, C programs are translated into an intermediate XML-based language named PiXL. The analysis is carried out on the PiXL representation, focussing on two aspects: extraction of every system call and control sequence, and analyzing every variable in the program in order to determine whether it should be inserted in the state vector. Creating the process graphs. In order to build the successor function that defines the implicit LTS of the program, a suitable representation of the processes composing the program is needed. To achieve this, every process is converted into a graph. Two kinds of transition labels are considered: labels of the first kind represent sequences of C statements (blocks) that do not include any system call, and labels of the second represent single system calls. System calls lead to nondeterministic behaviour, caused, e.g., by broken connections or by failures due to shortages of socket descriptors. Control statements in the C code that contain system calls have their structure appropriately translated in the process graph. These process graphs are built by the initialization primitive of the OPEN/CAESAR interface, which must be called before any other primitive of LTS exploration. Generating the implicit LTS. The states of the LTS are defined as state vectors containing the following information: local process variables, sockets, program counters, pids, and types of processes, etc. Transition labels contain the name of system calls and the data values passed as parameters to these calls. The algorithm for constructing the successor transitions of a state works in two steps: the first one explores, for every process graph, all the transitions going out from its current state; then, the second step fires each transition generated, by executing the corresponding code contained in the process graph, and updates the state vector accordingly.
Conclusions:	This proposal aims at defining a framework for model checking socket-based C programs by generating the implicit LTSs of these programs in conformance with the OPEN/CAESAR interface. Future work will consists in experimenting the tool on various case-studies and comparing the results with other existing approaches for verification of C programs.
Publications:	[Gallardo-Merino-Sanan-06] María del Mar Gallardo, Pedro Merino, and David Sanán. "Towards Model Checking C Code with OPEN/CAESAR". In J. Barjis, U. Ultes-Nitsche, and J. C. Augusto, editors, Proceedings of the 4th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems MSVVEIS'2006 (Paphos, Cyprus), INSTICC Press, pages 198-201, May 2006. Available on-line from the CADP Web site in PDF or PostScript [Gallardo-Merino-Sanan-07] María del Mar Gallardo, Pedro Merino, and David Sanán. "Extending CADP for Analyzing C Code". In Juan Carlos Augusto, Joseph Barjis, and Ulrich Ultes-Nitsche editors, Proceedings of the 5th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS-2007, In conjunction with ICEIS 2007, Funchal, Madeira, Portugal, June 2007, INSTICC Press, pp. 104-113, 2007. [Gallardo-Merino-Sanan-08] María del Mar Gallardo, Pedro Merino, and David Sanán. "Model Checking C Programs with Dynamic Memory Allocation". In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, IEEE, pp. 219-226, August 2008. Available on line at: http://www.computer.org/portal/web/csdl/doi/10.1109/COMPSAC.2008.143 or from the CADP Web site in PDF or PostScript
Contact:	Pedro Merino Associate Professor, PhD Dpto. de Lenguajes y Ciencias de la Computación ETSI Telecomunicación Universidad de Málaga Campus de Teatinos 29071 Málaga Spain Tel: +34 (5) 213 2752 Fax: +34 (5) 213 1397 E-mail: pedro@lcc.uma.es
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page