Organisation: 
LCC/GISUM, University of Málaga
and
Polytechnic University of València
(SPAIN)


Functionality: 
Static analysis and verification of concurrent C programs.

Tools used: 
CADP (Construction and Analysis of Distributed Processes)

Period: 
20062012

Description: 
The wellknown problem of state space explosion in model checking
is even more critical when applying this technique to programming
languages, mainly due to the presence of complex data structures.
Abstract matching is a recent technique for automatically
constructing smaller, yet accurate models (i.e., state spaces) of
programs. It consists in using an abstract matching function for
reducing the state vector by ignoring the variables whose values
are not relevant for checking a given property. Compared to classical
abstract interpretation methods, which construct an overapproximation
of the program model and therefore may introduce nonrealistic
execution paths, abstract matching creates an underapproximation
preserving exactly the execution paths required to check the property.
Abstract matching functions can be obtained automatically by using
static analysis techniques based upon computing the influence graph
for each variable in the program. This influence analysis can
be performed effectively by using model checking techniques.
Influence analysis works on the control flow graph of the program to be analyzed, represented as a labelled transition system (LTS). The states of this LTS correspond to program points (locations) and transitions are labelled by actions denoting boolean expressions and assignments occurring in the program statements. Influence analysis must determine, for each point p of the program, the set IA(p) of variables relevant for checking a given property. The authors show that, for a given program variable x and a specific kind of influence analysis, a program point p is influenced by x if its corresponding state in the LTS satisfies a certain formula expressed in the alternationfree mucalculus extended with data parameters. The sets IA(p) can be constructed by evaluating the mucalculus formula globally on the LTS for each variable x of the program. The set of points influenced by a variable x can also be obtained as the positive diagnostic (example) produced by evaluating onthefly a more refined mucalculus formula on the initial state of the LTS. This approach was experimented by encoding the LTS using the OPEN/CAESAR environment of CADP and evaluating the temporal formulas (expanded into plain mucalculus by Instantiating each value of their data parameters) using the EVALUATOR model checker. The ANNOTATOR tool, developed using the OPEN/CAESAR environment of CADP, implements a finergrained encoding of the influence analysis problem in terms of the local resolution of a parameterized boolean equation system (PBES). This more direct translation of the problem avoids the usage of a model checker and the interpretation of diagnostics. The LTS representing the control flow graph of the program is encoded according to the OPEN/CAESAR interface, which allows its onthefly exploration. The PBES underlying the influence analysis is expanded onthefly into a plain BES and solved using the CAESAR_SOLVE library of CADP. ANNOTATOR was successfully experimented on several examples of program flow graphs (encoded using the BCG format of CADP) and various kinds of influence analysis. 
Conclusions: 
The model checking and BES resolution techniques available in CADP
are shown to be effective solutions in the field of influence analysis.
Future work will concern the application of influence analysis to
large C programs in order to reduce their state spaces, as well as
the extension of ANNOTATOR with other kinds of static analysis.

Publications: 
[GallardoJoubertMerino06]
María del Mar Gallardo, Christophe Joubert, and Pedro Merino.
"Implementing Influence Analysis using Parameterised Boolean Equation
Systems". In Proceedings of the 2nd International Symposium on
Leveraging Applications of Formal Methods, Verification and Validation
ISOLA'06 (Paphos, Cyprus), IEEE Computer Society Press,
November 2006.
Available online at: http://www.dsic.upv.es/~joubert/publications/GallardoJoubertMerino06.pdf or from our FTP site in PDF or PostScript [GallardoJoubertMerino07] María del Mar Gallardo, Christophe Joubert, and Pedro Merino. "OntheFly Data Flow Analysis based on Verification Technology". In Proceedings of the 6th International Workshop on Compiler Optimization meets Compiler Verification COCV'07 (Braga, Portugal), Electronic Notes in Theoretical Computer Science 190(4), pp. 3348, March 2007. Available online at: http://www.dsic.upv.es/~joubert/publications/GallardoJoubertMerino07.pdf or from our FTP site in PDF or PostScript [GallardoJoubertMerinoSanan07a] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "OntheFly API Influence Analysis of Software". In Proceedings of the 2nd International Conference on Science and Technology JICT'2007 (Málaga, Spain), March 2007. Available online at: http://www.dsic.upv.es/~joubert/publications/GallardoJoubertMerinoSanan07a.pdf or from our FTP site in PDF or PostScript [GallardoJoubertMerinoSanan07b] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "C.OPEN and ANNOTATOR: Tools for OntheFly Model Checking C Programs". In Proceedings of the 14th International SPIN Workshop on Model Checking of Software SPIN'07 (Berlin, Germany), LNCS vol. 4595, pp. 268273, Springer Verlag, July 2007. Available online at: http://www.dsic.upv.es/~joubert/publications/GallardoJoubertMerinoSanan07c.pdf or from our FTP site in PDF or PostScript [GallardoJoubertMerinoSanan07c] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "OntheFly Model Checking for C Programs with Extended CADP in FMICSjETI". In Proceedings of the 12th IEEE International Conference on Engineering of Complex Computer Systems ICECCS'07 (Auckland, New Zealand), pp. 321329, IEEE Computer Society Press, July 2007. Available online at: http://www.dsic.upv.es/~joubert/publications/GallardoJoubertMerinoSanan07b.pdf or from our FTP site in PDF or PostScript [GallardoJoubertMerinoSanan12] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "A ModelExtraction Approach to Verifying Concurrent C Programs with CADP". Science of Computer Programming 77(3):375392, March 2012. Available online at: http://www.sciencedirect.com/science/article/pii/S0167642311001808/pdf?md5=d5f4a31bd82a9f5e6b1ffacf876a2bdf&pid=1s2.0S0167642311001808main.pdf 
Contact:  Christophe Joubert University of Málaga LCC/GISUM Campus de Teatinos s/n, 29071 Málaga Spain Tel: +34 952 13 71 99 Fax: +34 952 13 13 97 Email: joubert@lcc.uma.es 
Further remarks:  This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software 