The purpose of the project is to integrate in a remote and simple way new research tools developed at the University of Málaga. This will allow the static analysis and model checking of C programs into CADP, a popular toolbox for the design of communication protocols and distributed systems. An unexpected result of this project was the development of a Web service that remotely executes any verification tool (of which there are more than 42) or case study (more than 95) of CADP. This research consists in an FMICS Working Group contribution to the Verified Software Initiative (VSI), and resulted from a strengthened cooperation between the FMICS-jETI development group (University of Potsdam and Dortmund, Germany - Tiziana Margaria and Christian Kubczak) and the FMSE group (University of Málaga, Spain - María del Mar Gallardo, Jesús Martínez, Pedro Merino, David Sanán, and Christophe Joubert, the latter being now at Technical University of Valencia, Spain), in June 2006 at Málaga (Spain), June 2006 at IDPT'06 (San Diego, USA), November 2006 at ISOLA'06 (Paphos, Cyprus), and July 2007 at ICECCS'07 (Auckland, New Zealand). The research lines are also part of the Development of Automatic Techniques for Software Verification tasks of the SELF projects.
Our current research is working towards the direct connection of well-established verification toolboxes in a common environment, allowing easier access to efficient (unofficial/unreleased extensions of) verification tools and direct combinations of different formal technologies to solve a given problem. It is based on the FMICS-jETI platform for program verification, which is the new generation of ETI framework (ERCIM News No.36 - January 1999, 'ETI: An Online Service for Tool Coordination') associated with the International Journal on Software Tools for Technology Transfer (STTT), and is designed for interactive experimentation with and coordination of heterogeneous tools.
So far, the FMICS-jETI repository includes verification tools based on model-checking techniques, applications of model checking to dataflow analysis, parallel model checking, requirement elicitation, model synthesis, testing and automata learning. The follwing article in this issue shows how the strengths of the FMICS-jETI technology such as simple importing of the functionalities and workflows of a verification problem as SIBs (Service Independent Building blocks) can be successfully applied to interdisciplinary communities such as bioinformatics, and to problems like quantitative protein analysis.
In order to extend the FMICS-jETI repository to verification tools operating on Labelled Transition Systems (LTSs) extracted from C programs, we have designed atomic services (SIBs) for two new CADP tools. These are ANNOTATOR, for on-the-fly dataflow analysis of abstract program control flow graphs, and C.OPEN, for executing OPEN/CAESAR applications on C programs abstracted modulo a well-specified API. As a direct result of this project, an atomic service called SVL-PATH was created, which allows the remote execution of both I/O files and SVL scripts (a tool-independent coordination language on top of CADP, used for describing verification scenarios, including all invocations of over 42 available verification tools with appropriate options and parameters). We have shown the applicability of the approach by remotely analysing an implementation in C of Peterson's mutual exclusion protocol described by an SVL script. On a client machine executing the jABC framework, we have developed a generic process model, called Service Logic Graph (SLG), which permits the orchestration and choreography of seven atomic services to remotely execute any CADP case study through the SVL-PATH SIB. An important aspect of the approach is that CADP does not need to be altered to offer such service-oriented features. However, the method is currently limited by the fact that GUI tools cannot be directly integrated in the repository, meaning command line tools are preferred.
Concerning future activities, we expect to see the emergence of jETI servers in the FMICS community, offering program verification SIBs as well as running up-to-date verification toolboxes for remote use. A list of available public/private SIBs and corresponding jETI servers will also be published to allow their integration into complex verification process models.
Other ERCIM members cooperating and contributing to the FMICS-jETI platform include INRIA, STFC, CWI, ISTI-CNR and Masaryk University in Brno (CRCIM).
Links:
http://www.lcc.uma.es/gisum/tools/smc
http://jeti.cs.uni-dortmund.de/fmics
http://www.inrialpes.fr/vasy/fmics
http://www.inrialpes.fr/vasy/cadp
Please contact:
David Sanán
University of Malaga/SpaRCIM, Spain
Tel: +34 952 132846
E-mail: sanan
lcc.uma.es
