|
| 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 |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
CWI (THE NETHERLANDS)
Free University of Amsterdam (THE NETHERLANDS) Technical University of Eindhoven (THE NETHERLANDS) |
|---|---|
| Method: |
Chi
LTL (Linear-time Temporal Logic) mCRL (micro Common Representation Language) Promela regular alternation-free mu-calculus TCTL (Timed Computation Tree Logic) Timed Automata |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
mCRL toolset SPIN UPPAAL |
| Domain: |
Industrial Manufacturing Systems.
|
| Period: |
2004
|
| Size: |
25,926 states, 50,835 transitions
|
| Description: |
This case study compares different verification tools, using a
real-life turntable system as a benchmark example. The turntable is
specified in Chi, a modeling and simulation language for industrial
systems. Hence, for each of the considered verification tools, namely
SPIN, CADP (using mCRL as input language), and UPPAAL, the
difficulties in translating the Chi model to an input formalisam of
the tool, as well as the verification facilities are compared.
The turntable system consists of a round turntable, a clamp, a drill, and a testing device. The turntable has slots to transport products to the drill and the testing device. The drill drills holes in the products. After drilling a hole, the products are delivered to the testing device to ensure quality. The environment can add and remove products. The set of eight properties to be verified includes safety and liveness properties. The most complicated property is "every product eventually leaves the table", since it requires a fairness principle. As regards the generation of the state space, the case study shows that mCRL/CADP generated a state space (25,926 states and 50,835 transitions) almost 4 times smaller than the state space generated by SPIN (100,995 states and 188,724 transitions, using partial order reduction, statement merging and state vector compression). As regards the verification of the properties, the overall conclusion of the case study is that CADP provides the least number of problems and the most powerful language for expression of properties. |
| Conclusions: |
As regards modelling the turntable, sections 4.2, 5.2, and 6.2 of
[Bortnik-Trcka-Wijs-et-al-05] report difficulties in the translation
from Chi to Promela/SPIN, UPPAAL, and mCRL, since these three languages
lack nested parallelism (a feature of Chi that is supported by LOTOS).
As regards verification of properties, section 7 of the same paper concludes that using CADP is easier than SPIN and UPPAAL:
|
| Publications: |
[Bortnik-Trcka-Wijs-et-al-05]
E. Bortnik, N. Trcka, A.J. Wijs, S.P. Luttik, J.M. van de
Mortel-Fronczak, J.C.M. Baeten, W.J. Fokkink, and J.E. Rooda.
"Analyzing a Chi Model of a Turntable System using Spin, CADP and
UPPAAL". Journal of Logic and Algebraic Programming 65 (2),
November-December 2005.
Preliminary version available on-line at: http://alexandria.tue.nl/extra1/wskrap/publichtml/200423.pdf or from the CADP Web site in PDF 
or
PostScript 
[Mateescu-06-b] Radu Mateescu. "Modélisation et analyse de systèmes asynchrones avec CADP". In Nicolas Navet (ed.), Systèmes temps reél 1 --- techniques de description et de vérification, Traité IC2 chapter 5, pp. 151-180, Lavoisier, 2006 (in French). Full version available as INRIA Research Report RR 5953. Available on-line from http://cadp.inria.fr/publications/Mateescu-06-b.html [Mateescu-08] Radu Mateescu. "Specification and Analysis of Asynchronous Systems using CADP". In Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, chapter 5, ISTE publishing / John Wiley, ISBN 9781848210134, 2008. Available on-line from http://cadp.inria.fr/publications/Mateescu-08.html |
| Contact: | Anton Wijs CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam THE NETHERLANDS Tel: +31 (0)20 592 9333 Fax: +31 (0)20 592 4199 Email: A.J.Wijs@cwi.nl |
| Further remarks: |
Based on this case study, Radu Mateescu has written a LOTOS
specification of the turntable, which is available on-line at :
http://cadp.inria.fr/ftp/demos/demo_39
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page