Database of Case Studies Achieved Using CADP

Distributed Controller for the Production Cell Benchmark

Organisation: CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
VASY project-team, Inria Grenoble Rhône Alpes

Method: LNT
LOTOS

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

Domain: Manufacturing Systems.

Period: 1994-2017

Size: 1190 lines of LNT code
931 lines of LOTOS code
850 lines of C code

Description: 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.

Conclusions: 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.

Publications: [Garavel-Serwe-17] 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
or http://cadp.inria.fr/publications/Garavel-Serwe-17.html
Contact:
Hubert Garavel
Inria - LIG / CONVECS
655, avenue de l'Europe
CS 90051
38334 Montbonnot
FRANCE
Email: Hubert.Garavel@inria.fr
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 18:02:10 2018.

Back to the CADP case studies page