ANNOTATOR Tool for On-the-Fly Data Flow Analysis

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:	2006-2012
Description:	The well-known 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 over-approximation of the program model and therefore may introduce non-realistic execution paths, abstract matching creates an under-approximation 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 alternation-free mu-calculus extended with data parameters. The sets IA(p) can be constructed by evaluating the mu-calculus 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 on-the-fly a more refined mu-calculus 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 mu-calculus 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 finer-grained 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 on-the-fly exploration. The PBES underlying the influence analysis is expanded on-the-fly 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:	[Gallardo-Joubert-Merino-06] 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 on-line at: http://www.dsic.upv.es/~joubert/publications/Gallardo-Joubert-Merino-06.pdf or from the CADP Web site in PDF or PostScript [Gallardo-Joubert-Merino-07] María del Mar Gallardo, Christophe Joubert, and Pedro Merino. "On-the-Fly 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. 33-48, March 2007. Available on-line at: http://www.dsic.upv.es/~joubert/publications/Gallardo-Joubert-Merino-07.pdf or from the CADP Web site in PDF or PostScript [Gallardo-Joubert-Merino-Sanan-07-a] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "On-the-Fly API Influence Analysis of Software". In Proceedings of the 2nd International Conference on Science and Technology JICT'2007 (Málaga, Spain), March 2007. Available on-line at: http://www.dsic.upv.es/~joubert/publications/Gallardo-Joubert-Merino-Sanan-07-a.pdf or from the CADP Web site in PDF or PostScript [Gallardo-Joubert-Merino-Sanan-07-b] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "C.OPEN and ANNOTATOR: Tools for On-the-Fly 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. 268-273, Springer Verlag, July 2007. Available on-line at: http://www.dsic.upv.es/~joubert/publications/Gallardo-Joubert-Merino-Sanan-07-c.pdf or from the CADP Web site in PDF or PostScript [Gallardo-Joubert-Merino-Sanan-07-c] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "On-the-Fly Model Checking for C Programs with Extended CADP in FMICS-jETI". In Proceedings of the 12th IEEE International Conference on Engineering of Complex Computer Systems ICECCS'07 (Auckland, New Zealand), pp. 321-329, IEEE Computer Society Press, July 2007. Available on-line at: http://www.dsic.upv.es/~joubert/publications/Gallardo-Joubert-Merino-Sanan-07-b.pdf or from the CADP Web site in PDF or PostScript [Gallardo-Joubert-Merino-Sanan-12] María del Mar Gallardo, Christophe Joubert, Pedro Merino, and David Sanán. "A Model-Extraction Approach to Verifying Concurrent C Programs with CADP". Science of Computer Programming 77(3):375-392, March 2012. Available on-line at: http://www.sciencedirect.com/science/article/pii/S0167642311001808/pdf?md5=d5f4a31bd82a9f5e6b1ffacf876a2bdf&pid=1-s2.0-S0167642311001808-main.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 E-mail: joubert@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