|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web 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 |
Back to the CADP research tools page