T. Amagbegnon, P. Le Guernic, H. Marchand, E. Rutten. The Signal data flow methodology applied to a production cell. Rapport de recherche Irisa, No 917, Mars 1995.
Charger l'article :
Gziped Postscript
Copyright : Les documents contenus dans ces répertoires sont rendus disponibles par les auteurs qui y ont contribué en vue d'assurer la diffusion à temps de travaux savants et techniques sur une base non-commerciale. Les droits de copie et autres droits sont gardés par les auteurs et par les détenteurs du copyright, en dépit du fait qu'ils présentent ici leurs travaux sous forme électronique. Les personnes copiant ces informations doivent adhérer aux termes et contraintes couverts par le copyright de chaque auteur. Ces travaux ne peuvent pas être rendus disponibles ailleurs sans la permission explicite du détenteur du copyright.
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 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 imperative 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 Z/3Z for the formal proof of the satisfaction of application's requirements.
Keywords: Specification, verification, real-time systems, synchronous language, data flow, robotic production cell
Tochéou Amagbegnon
Hervé Marchand
Eric Rutten
@TechReport{amabegnon95b,
Author = {Amagbegnon, T. and Le Guernic, P. and Marchand, H. and Rutten, E.},
Title = {The Signal data flow methodology applied to a production cell},
Number = {917},
Institution = {Irisa},
Month = {March},
Year = {1995}
}
Charger la référence EndNote (.ref)
This page is part the Espresso project web site.
It has been automatically generated using the bib2html program.