Abstract
Our experience in using the RTGIL tools has shown that these tools and the graphical representation of the logic are very helpful for specifying and verifying properties of concurrent real-time systems. In addition to the aircraft example, we have used these tools to specify and verify properties of a railroad crossing system, a robot, an alarm system, and a four-phase handshaking protocol.
The RTGIL tools are implemented in Lucid Common Lisp and also in Franz Allegro Common Lisp, and require at least 32 MBytes of main memory and 64 Mbytes of swap space. The graphical editor was implemented using the Garnet graphics toolkit
This research was supported in part by NSF/ARPA grant CCR-9014382.
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 and D. Dill, “Automata for modelling real-time systems,” Proceedings of 17th International Conference on Automata Languages and Programming, Warwick University, England (July 1990), LNCS 443, Springer-Verlag, pp. 322–335.
D. L. Dill, “Timing assumptions and verification of finite-state concurrent systems,” Proceedings of International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France (June 1989), LNCS 407, Springer-Verlag, pp. 196–212.
B. A. Myers, D. A. Giuse, R. B. Danneberg, B. VanderZanden, D. S. Kosbie, E. Pervin, A. Mickish and P. Marchai, “Garnet: Comprehensive support for graphical, highly interactive user interfaces,” IEEE Computer (November 1990), pp. 71–85.
Y. S. Ramakrishna, L. K. Dillon, L. E. Moser, P. M. Melliar-Smith and G. Kutty, “A realtime interval logic and its decision procedure,” Proceedings of Thirteenth Conference on Foundations of Software Technology and Theoretical Computer Science, Bombay, India (December 1993), LNCS 761, Springer-Verlag, pp. 173–192.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moser, L.E., Melliar-Smith, P.M., Ramakrishna, Y.S., Kutty, G., Dillon, L.K. (1996). The Real-Time Graphical Interval Logic toolset. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_99
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_99
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive