Database of Research Tools Developed Using CADP

BFReduction and TEReduction Tools

Organisation: University of Malta

Functionality: Automatic generation of interfaces for model checking

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

Period: 2006

Description: A partial solution to the state space explosion problem is to use interfaces. An interface is essentially a group of states. Interfaces have up to now generally been defined manually, by an expert in the system or protocol to be verified.

Automatic interface generators have been created for two types of interface: a chaos state partition and a node behaviour state partition. A chaos state partition keeps a certain number of states and collapses the rest into a chaos state. The BFReduction tool can create a chaos state partition. Node behaviour state partitions group states according to their outgoing transitions. The TEReduction tool can create a node behaviour state partition. CADP was also used to create interfaces, using the node behaviour partition algorithm. The BCG tools of CADP were used for the implementation of the interface generators.

Studies of a reliable atomic multicast system (the rel/REL protocol) showed some reductions in the number of states using interfaces generated automatically with both methods. However the reductions from a manual interface were greater.

Conclusions: This proof-of-concept indicates the possibility of defining interfaces automatically. Further work will address the drawback of the current interface generation, and will extend the scope for automatic generation, with the ultimate goal of creating a general-purpose interface generator.

Publications: [Spina-Pace-06] Sandro Spina and Gordon Pace. "Automatic Interface Generation for Enumerative Model Checking". In John Abela, Angelo Dalli, and Kristian Guillaumier editors, Proceedings of the 4th Computer Science Annual Workshop CSAW'2006 (Msida, Malta), pp. 116-122, December 2006.
Full version available on-line from http://www.cs.um.edu.mt/gordon.pace/Research/Papers/csaw2006-03.pdf
or from our FTP site in PDF or PostScript
Contact:
Gordon J. Pace
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD 06,
MALTA
Tel: (+356) 2340 2504
Fax: (+356) 2132 0539
Email: Gordon.Pace@um.edu.mt



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page