University of Malta
Automatic generation of interfaces for model checking
CADP (Construction and Analysis of Distributed Processes)
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.
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
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
Gordon J. Pace
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD 06,
Tel: (+356) 2340 2504
Fax: (+356) 2132 0539
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|