Database of Case Studies Achieved Using CADP

Analysis of a Distributed System for Lifting Trucks.

Organisation: CWI / SEN2 (Amsterdam, THE NETHERLANDS)

Method: muCRL (micro Common Representation Language)

Tools used: muCRL toolset
CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded Software.

Period: 2000-2001

Size: about 450 lines of muCRL

Description: The process-algebraic language muCRL is used to analyse a real-life system for lifting trucks. The system consists of a number of lifts; each lift supports one wheel of the truck that is being lifted and has its own microcontroller. The controls of the different lifts are connected by means of a circular network. A special purpose protocol has been developed to let the lifts operate synchronously.

This system has been designed and implemented by a Dutch company. When testing the implementation the developers found three problems. They solved these problems in an ad hoc manner, although the causes of two of the three problems were unclear. Moreover, the developers were unsure that there were no other bugs hidden in the system. In close cooperation with the developers, the lift system was specified in muCRL, by striving to stay as close as possible to the actual implementation of the system.

Then, the resulting specification was analysed using the muCRL and CADP toolsets. The Labeled Transition Systems corresponding to the muCRL specification were generated using the muCRL tools and the correctness properties, expressed in regular alternation-free mu-calculus, were verified on the LTS models using the EVALUATOR 3.0 model-checker of CADP. The three known problems showed up in the specification (this is a strong indication that the specification represents closely enough the system). In addition, a fourth error was detected. This error was unknown and found its way into the implementation of the lift system. Various solutions for these problems were proposed and incorporated in the muCRL specification. After analyzing the new specification by model-checking, it was shown that it meets the requirements of the developers.

Conclusions: Four real errors were discovered in the design of a real system. Three of these problems were also found by the system developers in the test phase. The fourth problem was unknown and has found its way into the final release. For two of the three known problems, it was only known that the problem occurred but not what its causes were. The causes of those problems were discovered by using model-checking, and three of the four problems were solved (the last one is difficult to solve given the restrictions of the chosen hardware).

This case-study demonstrates that by using formal specification and automatic model-checking techniques, it is possible to improve the reliability of industrial safety-critical systems.

Publications: [Groote-Pang-Wouters-01] J.F Groote, J. Pang, and A.G. Wouters. "A Balancing Act: Analyzing a Distributed Lift System". Proceedings of the 6th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2001 (Paris, France), pp.1-12, June 2001. Full version available as CWI Report SEN-R0111, CWI, Amsterdam, May 2001.
Available on-line at: http://www.cwi.nl/static/publications/reports/abs/SEN-R0111.html
Contact:
Prof.dr.ir. J.F. Groote
Eindhoven University of Technology
Department of Computer Science
Systems Engineering
P.O. Box 513
NL-5600 MB Eindhoven
The Netherlands
Tel: +31 40 - 2475003
Tel: +31 40 - 2475010 (Secretary)
Fax: +31 40 - 2468508
E-mail: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 17:55:17 2018.

Back to the CADP case studies page