CWI / SEN2 (Amsterdam, THE NETHERLANDS)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
about 450 lines of muCRL
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.
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.
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
Prof.dr.ir. J.F. Groote
Eindhoven University of Technology
Department of Computer Science
P.O. Box 513
NL-5600 MB Eindhoven
Tel: +31 40 - 2475003
Tel: +31 40 - 2475010 (Secretary)
Fax: +31 40 - 2468508
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|