Abstract
We consider a new approach to synthesize abstract machines for reactive programs that interact with processes in order to achieve some control requirements in the context of the Supervisory Control Theory. The motivation behind our synthesis approach is related to the problem of scalability. Generally, synthesis procedures are based on a comparison of two state spaces (fixpoint calculation-based approach) or an exploration of a state space (search-based approach). In neither case do the synthesis procedures scale to specifications of realistic size. To circumvent this problem, we propose: i) to combine two formal notations for the representation of reactive programs in addition to the one for specifying control requirements; and ii) to integrate a synthesis procedure in a framework in which various transformations are applied with the sole aim of solving a smaller control problem from an abstract model.
The research described in this paper was supported in part by the Natural Sciences and Engineering Research Council of Canada (NSERC) and the Fonds pour la formation de chercheurs et léaide `a la recherche (FCAR).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Barbeau, F. Kabanza, and R. St-Denis, “A method for the synthesis of controllers to handle safety, liveness, and real-time constraints,” IEEE Trans. Automat. Contr., vol. 43, pp. 1543–1559, Nov. 1998.
J. P. Bowen, “The ethics of safety-critical systems,” Comm. of the ACM, vol. 43, pp. 91–97, April 2000.
Y.-L. Chen, S. Lafortune, and F. Lin, “How to reuse supervisors when discrete event system models evolve,” in Proc. of the 35th IEEE Conf. on Decision and Control, San Diago, CA, Dec. 1998, pp. 2964–2969.
S. L. Chung, S. Lafortune, and F. Lin, “Limited lookahead policies in supervisory control of discrete-event systems,” IEEE Trans. Automat. Contr., vol. 37, pp. 1921–1935, Dec. 1992.
J. E. R. Cury and B. H. Krogh, “Robustness of supervisors for discrete-event systems,” IEEE Trans. Automat. Contr., vol. 44, pp. 376–379, Feb. 1999.
H. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Berlin, Germany: Springer-Verlag, 1985.
J. A. Goguen and R. Diaconescu, “Towards an algebraic semantics for the object paradigm,” in Recent Trends in Data Type Specification, H. Ehrig and F. Orejas, Eds. Berlin, Germany: Springer-Verlag, 1992, Lecture Notes in Computer Science, vol. 785, pp. 1–26.
C. Heitmeyer, J. Kirby Jr., B. Labaw, M. Archer, and R. Bharadwaj, “Using abstraction and model checking to detect safety violations in requirements specifications,” IEEE Trans. Soft. Eng., vol. 24, pp. 927–947, Nov. 1998.
G. Huet, D. Oppen. “Equations and Rewrite Rules: A Survey.” in Formal Languages: Perspectives and Open Problems, R. Book, Ed. New York: Academic Press, 1980, pp. 349–405.
R. Koymans, “Specifying real-time properties with metric temporal logic,” Real-Time Syst., vol. 2, no. 4, pp. 255–299, 1990.
R. Kumar and V. K. Garg, Modeling and Control of Logical Discrete Event Systems. Boston, MA: Kluwer, 1995.
F. Lin, “Robust and adaptive supervisory control of discrete event systems,” IEEE Trans. Automat. Contr., vol. 38, pp. 1848–1852, Dec. 1993.
M. Makungu, M. Barbeau, and R. St-Denis, “Synthesis of controllers of processes modeled as colored Petri nets,” J. Discrete Event Dynamic Systems: Theory and Appl., vol. 9, no. 2, pp. 147–169, 1999.
P. J. G. Ramadge and W. M. Wonham, “The control of discrete event systems,” Proc. IEEE, vol. 77, pp. 81–98, 1989.
J. Rushby, “Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving,” in Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th Int. SPIN Workshops, D. Dams, R. Gerth, S. Leue, and M. Massink, Eds. Berlin, Germany: Springer-Verlag, 1999, Lecture Notes in Computer Science, vol. 1680, pp. 1–11.
J. Rushby, “Mechanized formal methods: where next?,” in FM’99-Formal Methods, J. M. Wing, J. Woodcock, and J. Davies, Eds. Berlin, Germany: Springer-Verlag, 1999, Lecture Notes in Computer Science, vol. 1708, pp. 48–51.
J. Sifakis, “Integration, the price of success,” in FM’99-Formal Methods, J. M. Wing, J. Woodcock, and J. Davies, Eds. Berlin, Germany: Springer-Verlag, 1999, Lecture Notes in Computer Science, vol. 1708, pp. 52–55.
R. St-Denis, “A formal method for the design of reactive systems,” in Proc. of the Int. Conf. on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Applications, Monastir, Tunisia, March 2000, Soft. Eng. Volume, pp. 1–6.
W. Thomas, “Automata on infinite objects,” in Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, J. van Leeuwen, Ed. Cambridge, MA: MIT Press, 1990, pp. 135–191.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frappier, M., St-Denis, R. (2001). Towards a Computer-Aided Design of Reactive Systems. In: Moreno-Díaz, R., Buchberger, B., Luis Freire, J. (eds) Computer Aided Systems Theory — EUROCAST 2001. EUROCAST 2001. Lecture Notes in Computer Science, vol 2178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45654-6_33
Download citation
DOI: https://doi.org/10.1007/3-540-45654-6_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42959-3
Online ISBN: 978-3-540-45654-4
eBook Packages: Springer Book Archive