CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
VASY project-team, Inria Grenoble Rhône Alpes
CADP (Construction and Analysis of Distributed Processes)
1190 lines of LNT code
931 lines of LOTOS code
850 lines of C code
This case study presents a distributed software controller for an
industrial production cell, replicating a real metal processing plant
in Karlsruhe, Germany. This case study was proposed in the 90s as a
popular benchmark to assess the benefits of different formal methods
applied to a common critical software system.
The production cell operates on metal plates (or blanks), which are brought into the cell by a feed belt, transported to a press via an elevating rotary table and a two-armed robot, before they leave the cell on the deposit belt. Diverging from the concrete production cell and to obtain a cyclic behaviour, the blanks are transported by a crane from the deposit back to the feed belt. The production cell is controlled by thirteen actuators (motors and magnets) and is equipped with fourteen sensors (switches, potentiometers, and photoelectric cells) to deliver status information to the controller. A graphical simulator, written in Tcl/Tk, enables prototype controllers to be validated and provides a reference to compare the controllers obtained from executable formal methods.
An early LOTOS specification of a controller for the production cell was developed in 1994, taking advantage of the multiway rendezvous and enabling the automatic generation of controller implementation in C. In 1997, a fully functional version with an operational connection to the simulator was integrated as a demonstration example to the CADP toolbox. In 2013, the LOTOS specification was simplified and translated to LNT, improving runtime performance. Both specifications have been further enhanced in 2017. To obtain a modular controller, each separately controllable device (or degree of freedom of a device) of the production cell is managed by a dedicated process, which are composed in parallel and synchronize by rendezvous to coordinate those movements involving several devices. The LOTOS and LNT models have been used to control the graphical simulator of the production cell for several days without detecting any problem.
This case study illustrates that the multiway rendezvous allows a
formal, concise, elegant, and modular description of a software
controller for manufacturing systems. In a concurrent setting,
high-level tasks can be simply decomposed into a set of processes that
execute simultaneously, only synchronizing themselves when some goals
of common interest have to be reached. As there can be more than two
such processes, multiway rendezvous is the paradigm of choice to
specify an atomic synchronization barrier governing all processes.
Hubert Garavel and Wendelin Serwe.
"The Unheralded Value of the Multiway Rendezvous: Illustration with the
Production Cell Benchmark".
Proceedings of the 2nd workshop on Models for Formal Analysis of Real
Systems (MARS 2017), Uppsala, Sweden. Electronic Proceedings in
Theoretical Computer Science, vol. 244, pages 230-270, April, 2017.
Available on-line at: http://eptcs.web.cse.unsw.edu.au/paper.cgi?MARS2017.10
Inria - LIG / CONVECS
655, avenue de l'Europe
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies