Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Gziped Postscript (.ps.gz)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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.
Hervé Marchand
hmarchan@irisa.fr
@TechReport{amabegnon95b,
Author = {Amagbegnon, T.P. 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}
}
Get EndNote Reference (.ref)