Abstract
In complex systems, like robot plants, applications are built on top of a set of components, or devices. Each of them has particular individual constraints, and there are also logical constraints on their interactions, related to e.g., mechanical characteristics or access to shared resources. Managing these constraints may be separated from the application, and performed by an intermediate layer.
We show how to build such property-enforcing layers, in a mixed imperative/declarative style: 1) the constraints intrinsic to one component are modeled by an automaton; the product of these automata is a first approximation of the set of constraints that should be respected; 2) the constraints that involve several components are expressed as temporal logic properties of this product; 3) we use general controller synthesis techniques and tools in order to combine the set of communicating parallel automata with the global constraint.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K. Altisen, G. Gößler, and J. Sifakis. Scheduler modelling based on the controller synthesis paradigm. Journal of Real-Time Systems, 23(1), 2002.
S. Balemi. Control of Discrete Event Systems: Theory and Application. PhD thesis, Automatic Control Laboratory, Swiss Federal Institute of Technology (ETH), Zurich, Switzerland, May 1992.
G. Berry. The foundations of esterel. Proof, Language and Interaction: Essays in Honour of Robin Milner, 2000. Editors: G. Plotkin, C. Stirling and M. Tofte.
A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and F.Y.C. Mang. Synchronous and bidirectional component interfaces. In CAV 2002: 14th International Conference on Computer Aided Verification, LNCS. Springer Verlag, 2002.
Aurélie Clodic. Tâches multi-modes et génération automatique de contrôleurs. Master thesis report, Institut National Polytechnique de Grenoble, June 2002. (in French).
Thomas Colcombet and Pascal Fradet. Enforcing trace properties by program transformation. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL-00). ACM Press, January 19-21 2000.
E.A. Emerson and E. Clarke. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. Workshop on Logic of Programs. LNCS 131, Springer Verlag, 1981.
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns. Addison Wesley, Reading, MA, 1995.
L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, 1977.
F. Maraninchi and N. Halbwachs. Compositional semantics of non-deterministic synchronous languages. In European Symposium On Programming, Linkoping (Sweden), April 1996. Springer verlag, LNCS 1058.
F. Maraninchi and Y. Rémond. Argos: an automaton-based synchronous language. Computer Languages, (27):61–92, 2001.
F. Maraninchi and Y. Rémond. Mode-automata: a new domain-specific construct for the development of safe critical systems. Science of Computer Programming, to appear, 2002.
H. Marchand, P. Bournai, M. Le Borgne, and P. Le Guernic. Synthesis of discreteevent controllers based on the Signal environment. Discrete Event Dynamical System: Theory and Applications, 10(4), October 2000.
Hervé Marchand and Éric Rutten. Managing multi-mode tasks with time cost and quality levels using optimal discrete control synthesis. In Proceedings of the 14th Euromicro Conference on Real-Time Systems, ECRTS’02, 2002.
Eric Rutten. A framework for using discrete control synthesis in safe robotic programming and teleoperation. In Proceedings of the IEEE International Conference on Robotics and Automation, ICRA’2001, 2001.
Eric Rutten and Hervé Marchand. Task-level programming for control systems using discrete control synthesis. Research Report 4389, INRIA, February 2002.
Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30–50, February 2000.
W. M. Wonham and P. J. Ramadge. On the supremal controllable sublanguage of a given language. SIAM Journal on Control and Optimization, 25(3):637–659, May 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Altisen, K., Clodic, A., Maraninchi, F., Rutten, E. (2003). Using Controller-Synthesis Techniques to Build Property-Enforcing Layers. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive