Abstract
Graphical Interval Logic is the foundation of a toolset we have developed to support formal specification and verification of concurrent systems. The logic is a discrete linear-time temporal logic with the distinguishing feature that formulas in the logic have an intuitive graphical representation. The toolset includes a graphical editor that allows the user to compose and edit graphical formulas on a workstation display and a theorem prover that mechanically checks the validity of proofs in the logic. This paper describes the toolset and illustrates its use.
This research was supported in part by NSF/DARPA grant CCR-9014382.
The paper was written by L. E. Moser and G. Kutty, who were responsible for the axiomatization of the logic and for the example. L. K. Dillon designed the graphical syntax of the logic and the graphical editor. G. Kutty implemented the graphical editor. Y. S. Ramakrishna devised the decision procedure and implemented the theorem prover. The original concept of Graphical Interval Logic is due to P. M. Melliar-Smith.
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
J. F. Allen, “Maintaining knowledge about temporal intervals,” Communications of the ACM 26, 11 (1983), 832–843.
P. A. Bernstein, V. Hadzilacos and N. Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley, Reading, MA, 1987.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill and L. J. Hwang, “Symbolic model checking: 1020 states and beyond,” Information and Computation 98 (1992), 142–170.
E. M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACM Trans. on Programming Languages and Systems 8, 2 (April 1986), 244–263.
J. Crow, S. T. Jefferson, R. Lee, P. M. Melliar-Smith, S. Owre, J. M. Rushby, R. L. Schwartz, N. Shankar, R. E. Shostak, F. W. von Henke and A. Whitehurst, “EHDM specification and verification system,” Technical Report, SRI International, Computer Science Laboratory, SRI Project 8110, January 1990.
L. K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith and Y. S. Ramakrishna, “Graphical specifications for concurrent software systems,” Proc. of 14th Intl. Conf. on Software Engineering, Melbourne, Australia (May 1992), 214–224.
D. Harel, H. Lackover, A Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring and M. Trakhtenbrot, “STATEMATE: A working environment for the development of complex reactive systems,” IEEE Trans. on Software Engineering 16, 4 (April 1990), 403–414.
The HOL System: Description, SRI International (December 1989).
S. Kono, “Automatic verification of interval temporal logic,” Proc. of 8th British Colloquium for Theoretical Computer Science (March 1992).
J. A. G. M. Koomen, “The TIMELOGIC temporal reasoning system,” Technical Report 231, Dept. of Computer Science, The University of Rochester, Rochester, NY, March 1989.
G. Kutty, L. E. Moser, P. M. Melliar-Smith, Y. S. Ramakrishna and L. K. Dillon, “Axiomatizations of interval logics,” submitted for publication.
L. Lamport, “A simple approach to specifying concurrent systems,” Communications of the ACM 32. 1 (January 1989), 32–45.
Z. Manna and A. Pnueli, “Verification of concurrent programs: The temporal framework,” Correctness Problem in Computer Science, R. S. Boyer, J. S. Moore (eds.), Academic Press (1981), 215–273.
Z. Manna and A. Pnueli, “Specification and verification of concurrent programs by ∀-automata,” Proc. of Conf. on Temporal Logic in Specification, LNCS 398, Altrincham, England (April 1987), 124–187.
B. Moszkowski and Z. Manna, “Reasoning in interval temporal logic,” Proc. of Workshop on Logics of Programs, LNCS 164, Springer-Verlag, Pittsburgh, PA (June 1983), 371–382.
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), 71–85.
I. Niemelä and H. Tuominen, “Helsinki Logic Machine: A system for logical expertise,” Technical Report B1, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, 1987.
Y. S. Ramakrishna, L. K. Dillon, L. E. Moser, P. M. Melliar-Smith and G. Kutty, “An automata-theoretic decision procedure for future interval logic,” Proc. of Twelfth Conf. on Foundations of Software Technology and Theoretical Computer Science, LNCS 652, Springer-Verlag, New Delhi, India (December 1992), 51–67.
R. Schlör and W. Damm, “Specification and verification of system-level hardware designs using timing diagrams,” Proc. of European Conf. on Design Automation, Paris, France (February 1993), 518–524.
P. Wolper, “The tableau method for temporal logic: An overview,” Logique et Analyse, Novelle Série 28e Année, 110–111 Numero Special, Automated Reasoning in Non-Classical Logic (June–September 1985), 119–136.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kutty, G., Ramakrishna, Y.S., Moser, L.E., Dillon, L.K., Melliar-Smith, P.M. (1993). A Graphical Interval Logic toolset for verifying concurrent systems. 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_12
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_12
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