|
| 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 Waterloo (CANADA)
|
|---|---|
| Functionality: |
Generation and minimization of labelled transition systems
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Period: |
2000
|
| Description: |
For large applications, model-checking techniques encounter the state
explosion problem, meaning that the size of the underlying state space
(or labelled transition system) may be exponential w.r.t. the size of
the application. A way to keep the state space manageable for
model-checkers is to include in the model only features that are
relevant to the property being checked. Such a model can be obtained
e.g., by hiding irrelevant actions and then minimizing the model
according to a suitable bisimulation relation, like observational
equivalence. Classical minimization algorithms require to construct
the whole state space and therefore are subject to state explosion.
Compositional and semi-compositional minimization algorithms attempt
to avoid this problem by minimizing components of the system
individually, but still may cause explosion in intermediate state
spaces because subsets of components need to be composed before being
minimized.
A new algorithm, called interaction abstraction algorithm, is proposed for constructing and minimizing labelled transition systems. The algorithm has similar goals to (semi-)compositional minimization, but attempts to use the information about interactions with the rest of the system to remove redundant information from the model, while keeping the information necessary to preserve the property being checked. The algorithm has a theoretical complexity of O (n^4 m^5) for a system with n components having m states maximum, but it seems to perform quite efficiently in practice. The algorithm has been implemented using the CADP toolset. Its behaviour is illustrated on a private branch exchange (PBX) software. On this case-study, the algorithm compared favourably with other model-checkers (SPIN, ARAPROD, and the EXHIBITOR and ALDEBARAN tools of CADP), by allowing to handle a PBX specification with 5 components. |
| Conclusions: |
An original approach for minimizing labelled transition systems modulo
observational equivalence, called interaction abstraction, has been
proposed and implemented using CADP. The algorithm is most useful when
models of systems deal with many aspects, but only one aspect is of
interest at a time. Interaction abstraction can be used in conjunction
with other reduction techniques (e.g., compositional minimization,
on-the-fly search, or partial-order reduction) in order to take a
better advantage of the redundancy that may be present in systems.
Further research is needed in order to extend the algorithm with other
equivalence relations (e.g., safety equivalence) and to allow a better
behaviour in the case of systems with many components.
|
| Publications: |
[Liu-00]
Wayne Liu.
"Interaction Abstraction for Compositional Finite State Systems".
In K. Havelund, J. Penix, and W. Visser, editors, Proceedings of
the 7th SPIN Workshop (Stanford University, California), LNCS
vol. 1885, pp. 148-162, Springer Verlag, September 2000.
Available on-line at: http://netlib.bell-labs.com/netlib/spin/ws00/18850150.pdf or also from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Wayne Liu Electrical and Computer Engineering Department University of Waterloo Waterloo, Ontario, Canada, N2L 3G1 Tel: (519) 888-4567x5167 Fax: (519) 746-3077 E-mail: wbliu@uwaterloo.ca |
| 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