Abstract
Our aim is to specify, verify and implement a controller for a production cell, using the Signal approach. Our contribution to this case study aims at illustrating the methodology associated with the Signal synchronous data flow language for the programming of control systems, as well as how dynamical properties can be proved using the tool Signal. Hence, we describe the full development of the example, specifying a generic controller, safe for all scheduling scenarios. The specification is made in terms of events and boolean data, abstracting from the numerical nature of some of the sensor data; this enables the use of Signal for the formal proof of the application's requirements satisfaction.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
T. P. Amagbegnon, P. Le Guernic, H. Marchand, E. Rutten, Specification, Implementation and Verification of a Production Cell with Signal. IRISA/INRIA-Rennes, research report. (to appear)
P. Bournai, P. Le Guernic Un environnement graphique pour le langage signal. IRISA/ INRIA-Rennes, research report N∘741, July 1993. (In French)
B. Dutertre. Spécification et preuve de systèmes dynamiques. Ph.D. thesis, University of Rennes 1, France, December 1992. (In French)
M. Le Borgne, B. Dutertre, A. Benveniste and P. Le Guernic. Dynamical Systems over Galois Fields, In Proc. of the Second European Control Conference (ECC 93), Groningen, 1993.
P. Le Guernic, T. Gautier, M. Le Borgne, C. Le Maire. Programming Real-Time Applications with signal. Another look at real-time programming, special section of Proceedings of the IEEE, 79(9), September 1991.
H. J. Touati, H. Sajov, B. Lin, R. K. Brayton and A. Sangiovanni-Vincentelly, Implicit state enumeration of finite state machines using BDD's, International Conference on Computer-Aided Design, IEEE, November 1990, p. 130–133.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Amagbegnon, T.P., Le Guernic, P., Marchand, H., Rutten, É. (1995). Signal. In: Lewerentz, C., Lindner, T. (eds) Formal Development of Reactive Systems. Lecture Notes in Computer Science, vol 891. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58867-1_51
Download citation
DOI: https://doi.org/10.1007/3-540-58867-1_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58867-2
Online ISBN: 978-3-540-49133-0
eBook Packages: Springer Book Archive