Abstract
We present a synchronous approach to real-time reactive programming in Lucid enriched with contexts as first class objects. The declarative intensional approach allows real-time reactive programs to manipulate both events and state-based representations of complex systems. We show the formal specification of the Train-Gate-Controller problem, a standard case study in real-time systems community, and formally verify the safety property.
This work is supported by grants from the Natural Sciences and Engineering Research Council of Canada.
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.
References
Alagar, V.S., Paquet, J., Wan, K.: Intensional programming for agent communication. In: Leite, J., Omicini, A., Torroni, P., Yolum, p. (eds.) DALT 2004. LNCS (LNAI), vol. 3476, pp. 239–255. Springer, Heidelberg (2005)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: A declarative language for programming synchronous systems. In: P.O.P.L (1987)
Guha, R.V.: Contexts: A Formalization and Some Applications. Ph.d thesis, Stanford University (February 10, 1995)
Heitmeyer, C., Lynch, N.: The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems. In: Proceedings of the 15th IEEE Real-time Systems Symposium, RTSS 1994, San Juan, Puerto Rico, December 1994, pp. 120–131 (December 1994)
Marchand, H., Rutten, E., Le Borgne, M., Samman, M.: Formal verification of programs specified with signal: application to a power transformer station controller. Science of Computer Programming 41, 85–104 (2001)
Muthiayen, D.: Real-Time Reactive System Development - A Formal Approach Based on UML and PVS. Phd. Thesis, Department of Computer Science, Concordia University, Montreal, Canada (January 2000)
Paquet, J., Kropf, P.G.: The GIPSY architecture. In: Kropf, P.G., Babin, G., Plaice, J., Unger, H. (eds.) DCW 2000. LNCS, vol. 1830, pp. 144–153. Springer, Heidelberg (2000)
Paquet, J.: Intensional Scientific Programming Ph.D. Thesis, Département d’Informatique, Universite Laval, Quebec, Canada (1999)
Paquet, J., Plaice, J.: Dimensions and functions as values. In: Proceedings of the Eleventh International Symposium on Lucid and Intensional Programming, Sun Microsystems, Palo Alto, California, USA (1998)
Plaice, J.: RLucid, a general real-time dataflow language. Formal Techniques in Real- Time and Fault-Tolerant Systems, Berlin, pp. 363–374 (1992)
Springintveld, J., Vaandrager, F., Dargenio, P.: Testing Timed Automata. Theoretical Computer Science 254, 225–257 (2001)
Wadge, W.W., Ashcroft, E.A.: Lucid, the dataflow programming language. Academic Press, London (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wan, K., Alagar, V., Paquet, J. (2005). Real Time Reactive Programming in Lucid Enriched with Contexts. In: Liu, Z., Araki, K. (eds) Theoretical Aspects of Computing - ICTAC 2004. ICTAC 2004. Lecture Notes in Computer Science, vol 3407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31862-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-31862-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25304-4
Online ISBN: 978-3-540-31862-0
eBook Packages: Computer ScienceComputer Science (R0)