Distributed system for lifting trucks

From MCRL2

μ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.

Contents 1 Technical details 1.1 Type of verification 1.2 Data size 1.3 Equipment (computers, CPU, RAM) 1.4 Models 2 Organizational context 2.1 Contact person 2.2 Other people involved 2.3 Institution 2.4 Industrial partner 2.5 Time period 3 Publications 4 Links

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.

Data size

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

Industrial partner

Add-Controls, Amersfoort, The Netherlands

Time period

Around 2000

Publications

Analysis of a distributed system for lifting trucks. Jan Friso Groote, Jun Pang, and Arno Wouters. Journal of Logic and Algebraic Programming, 55(1-2): 21-56, 2003.

Links

[1] contains another description of this showcase.