GISUM, University of Málaga (SPAIN)
Software Model Checking
CADP (Construction and Analysis of Distributed Processes)
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:
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.
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 our FTP 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 our FTP site in PDF or PostScript
Associate Professor, PhD
Dpto. de Lenguajes y Ciencias de la Computación
Universidad de Málaga
Campus de Teatinos
Tel: +34 (5) 213 2752
Fax: +34 (5) 213 1397
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|