CWI (THE NETHERLANDS)
Free University of Amsterdam (THE NETHERLANDS)
Technical University of Eindhoven (THE NETHERLANDS)
LTL (Linear-time Temporal Logic)
mCRL (micro Common Representation Language)
regular alternation-free mu-calculus
TCTL (Timed Computation Tree Logic)
CADP (Construction and Analysis of Distributed Processes)
Industrial Manufacturing Systems.
25,926 states, 50,835 transitions
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.
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:
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),
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
CWI / Department of Software Engineering
SEN2 (Specification and Analysis of Embedded Systems)
Kruislaan 413, 1098 SJ Amsterdam
Tel: +31 (0)20 592 9333
Fax: +31 (0)20 592 4199
Based on this case study, Radu Mateescu has written a LOTOS
specification of the turntable, which is available on-line at :
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies