Distributed system for lifting trucks

../../_images/Lift.jpeg

µCRL was used in the analysis of a real-life system for lifting trucks (lorries, railway carriages, buses and other vehicles). 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 cyclical network. A special purpose protocol has been developed to let the lifts operate synchronously. Four errors were found in the original design. A solution to these problems was proposed and it was shown by means of model checking that the modified system meets the requirements.

Technical details

Two safety, two liveness properties and deadlock freedom were checked.

Type of verification

Deadlock and safety properties violations detection by explicit state-space generation (breadth-first search). CADP toolset was used to model-check the properties formulated in regular alternation-free modal µ-calculus.

Equipment (computers, CPU, RAM)

Models

The model is available as a part of the µCRL Toolset. A translation of this model to mCRL2, performed by Bas Ploeger, is distributed with the mCRL2 Toolset.

Organizational context
Contact person:

Jun Pang

Other people involved:

  • Bert Lisser (CWI)

  • Jan Friso Groote (TU/e)

  • Arno Wouters

Institution:

CWI, Amsterdam, The Netherlands

Industrial partner:

Add-Controls, Amersfoort, The Netherlands

Time period:

Around 2000

Publications

[GPW03]