Skip to Main content Skip to Navigation

The Signal data flow methodology applied to a production cell

Tochéou Amagbegnon 1 Paul Le Guernic 1 Hervé Marchand 1 Eric Rutten 1
1 EP-ATR - Environnement de programmation d'applications temps réel
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : This report presents a method to specify, verify and implement a controller for a robotic production cell using the Signal approach. This work has been performed as part of a case study concerning a production cell, proposed by {\sc FZI} of Karlsruhe. Our contribution to this case study aims at illustrating the methodology associated with the \signal synchronous data flow language for the specification and implementation of control systems, as well as the verification of statical and dynamical properties using a proof system for \signal programs. We describe the full development of the example, specifying a generic controller, safe for all scheduling scenarios. The specification is structured in a modular way, using two decomposition principles: one following the architecture of the production cell, the other one separating the controller from the model of the system to be controlled. The latter point lies the originality of the approach, compared to imperativ- e methods: the declarative language is used to specify, in the form of equations on signals, the behaviour of a system, and a controller putting constraints on it This way, one can build hierarchies of nested controlled systems: in the case of the production cell, the scheduled behaviour is a controlled instance of the safe behaviour, which is itself a controlled instance of the natural behaviour. The model of the production cell is made in terms of events and boolean data, abstracting from the numerical nature of part of the sensor data; this enables the formal analysis of the logical properties of the system. The equational nature of the \signal language leads naturally to the use of methods based on systems of polynomial dynamic equations over \zzz for the formal proof of the satisfaction of application's requiremen- ts.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:37:53 PM
Last modification on : Friday, February 4, 2022 - 3:23:18 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:06:10 AM


  • HAL Id : inria-00074155, version 1


Tochéou Amagbegnon, Paul Le Guernic, Hervé Marchand, Eric Rutten. The Signal data flow methodology applied to a production cell. [Research Report] RR-2522, INRIA. 1995. ⟨inria-00074155⟩



Record views


Files downloads