A graphical interval logic for specifying concurrent systems

ABSTRACT

This article describes a graphical interval logic that is the foundation of a tool set supporting formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to understand and use. The objective of this article is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of the graphical logic, the article provides some specifications for an elevator system and proves several properties of the specifications. The article also describes the tool set and the implementation.

REFERENCES

• 1: A. A. Aaby , K. T. Narayana, Propositional Temporal Interval Logic is PSPACE Complete, Proceedings of the 9th International Conference on Automated Deduction, p.218-237, May 23-26, 1988
• 2: Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984 [doi>10.1145/800057.808665]
• 3: ~DILLON, L. K., KUTTY, G., MELLIAR-SMITH, P. M., MOSER, L. E., AND RAMAKRISHNA, Y.S. 1994. ~Visual specifications for temporal reasoning. J. Vis Lang. Comput. 5, 1, 61-81.
• 4: L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, A Graphical Interval Logic for Specifying Concurrent Systems, University of California at Santa Barbara, Santa Barbara, CA, 1993
• 5: L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, Graphical specifications for concurrent software systems, Proceedings of the 14th international conference on Software engineering, p.214-224, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143116]
• 6: Dov M. Gabbay, The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems, Temporal Logic in Specification, p.409-448, April 08-10, 1987
• 7: A. Giacalone , S. A. Smolka, Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems, IEEE Transactions on Software Engineering, v.14 n.6, p.787-802, June 1988 [doi>10.1109/32.6158]
• 8: ~GILLETT, W. U., AND KIMURA, T.D. 1986. Parsing two-dimensional languages. In Proceedings ~of the IEEE lOth Internatzonal Conference of Computer Software and Applications. IEEE, New ~York, 472-477.
• 9: ~GOUN, E. AND RErSS, S P. 1989. The specification of visual language syntax. In Proceedings of ~the IEEE Workshop on Visual Languages, IEEE, New York, 105-110.
• 10: Joseph Y. Halpern , Yoav Shoham, A propositional modal logic of time intervals, Journal of the ACM (JACM), v.38 n.4, p.935-962, Oct. 1991 [doi>10.1145/115234.115351]
• 11: Joseph Y. Halpern , Zohar Manna , Ben C. Moszkowski, A Hardware Semantics Based on Temporal Intervals, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.278-291, July 18-22, 1983
• 12: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 13: David Harel , Amir Pnueli , Hagi Lachover , Amnon Naamad , Michal Politi , Rivi Sherman , Aharon Shtull-Trauring , Mark Trakhtenbrot, STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.403-414, April 1990 [doi>10.1109/32.54292]
• 14: ~KOOMEN, J. A. G.M. 1987. The TIMELOGIC temporal reasoning system. Tech. Rep., Dept. of ~Computer Science, Umv. of Rochester, N.Y. (Revised March 1989).
• 15: ~KUTTY, G. 1993. A tool for the interactive generation of Graphical Interval Logic formulas. ~Tech. Rep, 9307, Dept. of Electrical and Computer Engineering, Univ. of California, Santa ~Barbara, Cahf.
• 16: G. Kutty , Louise E. Moser , P. M. Melliar-Smith , Laura K. Dillon , Y. S. Ramakrishna, First-Order Future Interval Logic, Proceedings of the First International Conference on Temporal Logic, p.195-209, July 11-14, 1994
• 17: G. Kutty , Y. S. Ramakrishna , Louise E. Moser , Laura K. Dillon , P. M. Melliar-Smith, A Graphical Interval Logic Toolset for Verifying Concurrent Systems, Proceedings of the 5th International Conference on Computer Aided Verification, p.138-153, June 28-July 01, 1993
• 18: ~LAMPORT, L. 1990. A temporal logic of actions. Tech. Rep. 57, DEC Systems Research Center, ~Palo Alto, Calif.
• 19: ~LAMPOm', L. 1983. What good is temporal logic? In Proceedings of the IFIP Congress. IFIP, ~Washington, D.C., 657-668.
• 20: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 21: Zohar Manna , Amir Pnueli, Specification and Verification of Concurrent Programs by forall-Automata, Temporal Logic in Specification, p.124-164, April 08-10, 1987
• 22: ~MANNA, Z., AND PNUELI, A. 1981. Verification of concurrent programs: The temporal frame- ~work. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. ~Academic Press, New York, 215-273.
• 23: P. M. Melliar-Smith, A graphical representation of interval logic, International Conference on Concurrency on Concurrency 88, p.106-120, October 1988, Hamburg, Germany
• 24: Brad A. Myers , Dario A. Giuse , Roger B. Dannenberg , David S. Kosbie , Edward Pervin , Andrew Mickish , Brad Vander Zanden , Philippe Marchal, Garnet: Comprehensive Support for Graphical, Highly Interactive User Interfaces, Computer, v.23 n.11, p.71-85, November 1990 [doi>10.1109/2.60882]
• 25: David A. Plaisted, A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.403-420, June 06-08, 1983
• 26: Vaughan Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, v.15 n.1, p.33-71, Feb. 1986 [doi>10.1007/BF01379149]
• 27: Y. Srinivas Ramakrishna, Interval logics for temporal specification and verification, University of California at Santa Barbara, Santa Barbara, CA, 1994
• 28: Y. S. Ramakrishna , Laura K. Dillon , Louise E. Moser , P. M. Melliar-Smith , G. Kutty, A Real-Time Interval Logic and Its Decision Procedure, Proceedings of the 13th Conference on Foundations of Software Technology and Theoretical Computer Science, p.173-192, December 15-17, 1993
• 29: ~RAMAKRISHNA, Y. S., MELLIAR-SMITH, P. M., MOSER, L. E., DILLON, L. K., AND KUTTY, G. 1993b. ~Really visual temporal reasoriing. In Proceedings of the 14th IEEE Real-Time Systems Sympo- ~sium, IEEE, New York, 262-273.
• 30: Y. S. Ramakrishna , Laura K. Dillon , Louise E. Moser , P. M. Melliar-Smith , G. Kutty, An Automata-Theoretic Decision Procedure for Future Interval Logic, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.51-67, December 18-20, 1992
• 31: ~SCHLC)R, R., AND DAMM, W. 1993. Specification of system-level hardware designs using timing ~diagrams. In Proceedings of the European Conference on Design Automation a,d European ~Event in ASIC Design. IEEE Computer Society Press, Los Alamitos, Calif., 518-524.
• 32: Richard L. Schwartz , P. M. Melliar-Smith , Friedrich H. Vogt, An interval logic for higher-level temporal reasoning, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.173-186, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806720]
• 33: Pierre Wolper, On the Relation of Programs and Computations to Models of Temporal Logic, Temporal Logic in Specification, p.75-123, April 08-10, 1987

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages; Tools

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Human Factors, Languages, Theory, Verification

Keywords:
automated proof-checking, concurrent systems, formal specifications, graphical interval logic, temporal logic, timing diagrams, visual languages