Database of Case Studies Achieved Using CADP

Analysis of a Turntable System

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:
    "Overall we conclude that CADP provides the least number of problems concerning the verification of the properties."


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 our FTP 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 : ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_39

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page