Abstract
We propose to apply the verification techniques available for Timed Graphs [ACD90], and particularly the symbolic model-checking algorithm of [HNSY92], to the Argos [Mar92] synchronous language. We extend the language with a single delay construct that allows to express watchdogs and timeouts, at any level in the parallel or hierarchic structure of a program. We define the semantics of this extended language in terms of Timed Graphs, and show that it is a “convenient” extension of the pure Argos synchronous semantics. Indeed, for discrete time, the two semantics coincide. The Timed Graph semantics can be viewed as a continuous time semantics for Argos. We extend the Argos compiler and connect it to the KRONOS tool which implements the abovementioned model-checking algorithm.
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
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the fifth annual IEEE symposium on Logics In Computer Science, pages 414–425, Philadelphie, PA, USA, June 1990.
G. Berry and G. Gonthier. The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation. Technical Report, 842, INRIA, 1988.
G. Berry and G. Gonthier. The Esterel synchronous programming language: design, semantics, implementation. Science Of Computer Programming, 19(2):87–152, 1992.
P. Caspi, N. Halbwachs, D. Pilaud, and J. Plaice. Lustre, a declarativelanguage for programming synchronous systems. In 14th Symposium on Principles of Programming Languages, january 1987.
P. Le Guernic, A. Benveniste, P. Bournai, and T. Gauthier. Signal: A Data Flow Oriented Language for Signal Processing. Technical Report, IRISA report 246, IRISA, Rennes, France, 1985.
D. Harel. Statecharts: a visual approach to complex systems. Science of Computer Programming, 8:231–275, 1987.
T. Henzinger. X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In LICS'92, June 1992.
F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. In CONCUR, LNCS 630, Springer Verlag, august 1992.
F. Maraninchi and M. Vachon. An experience in compiling a mixed imperative/declarative language for reactive systems. In International Workshop on Compiler Construction (poster session), Springer Verlag, LNCS 641, October 1992.
X. Nicollin, J. Sifakis, and S. Yovine. From ATP to Timed Graphs and Hybrid Systems. In J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, editors, LNCS 600, proceedings of REX Workshop “Real-Time: Theory in Practice”. Mook, The Nederlands, Springer Verlag, June 1991.
X. Nicollin, J. Sifakis, and S. Yovine. Compiling real-time specifications into timed automata. IEEE Transactions on Software Engineering, special issue on Specification and Analysis of Real-Time Systems, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jourdan, M., Maraninchi, F., Olivero, A. (1993). Verifying quantitative real-time properties of synchronous programs. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_29
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive