A graphical environment for the design of concurrent real-time systems

ABSTRACT

Concurrent real-time systems are among the most difficult systems to design because of the many possible interleavings of events and because of the timing requirements that must be satisfied. We have developed a graphical environment based on Real-Time Graphical Interval Logic (RTGIL) for specifying and reasoning about the designs of concurrent real-time systems. Specifications in the logic have an intuitive graphical representation that resembles the timing diagrams drawn by software and hardware engineers, with real-time constraints that bound the durations of intervals. The syntax-directed editor of the RTGIL environment enables the user to compose and edit graphical formulas on a workstation display; the automated theorem prover mechanically checks the validity of proofs in the logic; and the database and proof manager tracks proof dependencies and allows formulas to be stored and retrieved. This article describes the logic, methodology, and tools that comprise the prototype RTGIL environment and illustrates the use of the environment with an example application.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, An old-fashioned recipe for real time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1543-1571, Sept. 1994 [doi>10.1145/186025.186058]
• 2: Martín Abadi , Leslie Lamport, Conjoining specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.3, p.507-535, May 1995 [doi>10.1145/203095.201069]
• 3: Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
• 4: Rajeev Alur , Thomas A. Henzinger, Real-time logics: complexity and expressiveness, Information and Computation, v.104 n.1, p.35-77, May 1993 [doi>10.1006/inco.1993.1025]
• 5: Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996 [doi>10.1145/227595.227602]
• 6: Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996 [doi>10.1109/32.489079]
• 7: Nikolaj Bjorner , Anca Browne , Eddie Chang , Michael Colon , Arjun Kapur , Z Manna , Henny B. Sipma , Tomas E. Uribe, STeP: The Stanford Temporal Prover (Educational Release) User''s Manual, Stanford University, Stanford, CA, 1995
• 8: S. Campos , E. Clarke , W. Marrero , M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems, ACM SIGPLAN Notices, v.30 n.11, p.70-78, Nov. 1995
• 9: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 10: CLEMENTS, P. C., HEITMEYER, C. L., LABAW, B. G., AND ROSE, A.T. 1993. MT: A toolset for specifying and analyzing real-time systems. In Proceedings of the 14th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Los Alamitos, Calif., 12-22.
• 11: Costas Courcoubetis , David L. Dill , Magda Chatzaki , Panagiotis Tzounakis, Verification with Real-Time COSPAN, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.274-287, June 29-July 01, 1992
• 12: CROW, J., JEFFERSON, S. T., LEE, R., MELLIAR-SMITH, P. M., OWRE, S., RUSHBY, J. M., SCHWARTZ, R. L., SHANKAR, N., SHOSTAK, R. E., VON HENKE, F. W., AND WHITEHURST, A. 1990. EHDM specification and verification system. Tech. Rep. SRI Project 8110, Computer Science Laboratory, SRI International, Menlo Park, Calif. Jan.
• 13: D. L. Dill, Timing assumptions and verification of finite-state concurrent systems, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.197-212, February 1990, Grenoble, France
• 14: L. K. Dillon , G. Kutty , L. E. Moser , P. M. Melliar-Smith , Y. S. Ramakrishna, A graphical interval logic for specifying concurrent systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.2, p.131-165, April 1994 [doi>10.1145/192218.192226]
• 15: Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.308-339, Oct. 1994 [doi>10.1145/201024.201034]
• 16: Kathi D. Fisler, Exploiting the potential of diagrams in guiding hardware reasoning, Logical reasoning with diagrams, Oxford University Press, Inc., New York, NY, 1996
• 17: C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
• 18: HAR'EL, Z. AND KURSHAN, R. 1990. Software for analytical development of communications protocols. AT&T Tech. J. 69, 1 (Jan./Feb.), 45-59.
• 19: 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]
• 20: HAREL, D., KOZEN, D., AND PARIKH, R. 1982. Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci. 25, 2 (Oct.), 145-180.
• 21: 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]
• 22: Thomas A. Henzinger , Xavier Nicollin , Joseph Sifakis , Sergio Yovine, Symbolic model checking for real-time systems, Information and Computation, v.111 n.2, p.193-244, June 1994 [doi>10.1006/inco.1994.1045]
• 23: Farnam Jahanian , Aloysius K. Mok, Modechart: A Specification Language for Real-Time Systems, IEEE Transactions on Software Engineering, v.20 n.12, p.933-947, December 1994 [doi>10.1109/32.368134]
• 24: Yonit Kesten , Zohar Manna , Amir Pnueli, Verifying clocked transition systems, Proceedings of the DIMACS/SYCON workshop on Hybrid systems III : verification and control: verification and control, p.13-40, July 1996, New Brunswick, NeW Jersey, United States
• 25: KOEDINGER, K. R. AND ANDERSON, g. R. 1990. Abstract planning and perceptual chunks: Elements of expertise in geometry. Cog. Sci. 14, 4 (Oct./Dec.), 511-550.
• 26: Ron Koymans , Jan Vytopil , Willem P. de Roever, Real-time programming and asynchronous message passing, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.187-197, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806721]
• 27: KUTTY, G., MOSER, L. E., MELLIAR-SMITH, P. M., RAMAKRISHNA, Y. S., AND DILLON, L.K. 1995. Axiomatizations of interval logics. Fundamenta Informaticae 24, 4 (Dec.), 313-332.
• 28: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 29: Leslie Lamport, TLA in Pictures, IEEE Transactions on Software Engineering, v.21 n.9, p.768-775, September 1995 [doi>10.1109/32.464544]
• 30: T. F. Lunney , R. H. Perrott, Syntax-directed editing, Software Engineering Journal, v.3 n.2, p.37-46, March 1988
• 31: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 32: Zohar Manna , Amir Pnueli, Temporal Verification Diagrams, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.726-765, April 19-22, 1994
• 33: P. M. Melliar-Smith, A graphical representation of interval logic, International Conference on Concurrency on Concurrency 88, p.106-120, October 1988, Hamburg, Germany
• 34: L. E. Moser , P. M. Melliar-Smith, Formal verification of safety-critical systems, Software—Practice & Experience, v.20 n.9, p.799-811, August 1990
• 35: Louise E. Moser , P. M. Melliar-Smith, Consistent composition and refinement for dependable systems, Proceedings of the second international conference on Mathematics of dependable systems II, p.15-27, February 1998, Univ. of York, England
• 36: 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]
• 37: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
• 38: Y. S. Ramakrishna , P. M. Melliar-Smith , L. E. Moser , L. K. Dillon , G. Kutty, Interval logics and their decision procedures: part I: an interval logic, Theoretical Computer Science, v.166 n.1-2, p.1-47, Oct. 20, 1996 [doi>10.1016/0304-3975(95)00254-5]
• 39: Y. S. Ramakrishna , P. M. Melliar-Smith , L. E. Moser , L. K. Dillon , G. Kutty, Interval logics and their decision procedures: part I: an interval logic, Theoretical Computer Science, v.166 n.1-2, p.1-47, Oct. 20, 1996 [doi>10.1016/0304-3975(95)00254-5]
• 40: A. P. Atlee , H. Gannon, Specifying and Verifying Requirements of Real-Time Systems, IEEE Transactions on Software Engineering, v.19 n.1, p.41-55, January 1993 [doi>10.1109/32.210306]
• 41: SCHL()R, R. AND DAMM, W. 1993. Specification and verification of system-level hardware designs using timing diagrams. In Proceedings of the European Conference on Design Automation. IEEE Computer Society Press, Los Alamitos, Calif., 518-524.
• 42: Richard L. Schwartz , P. M. Melliar-Smith , Friedrich H. Vogt, An Interval-Based Temporal Logic, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.443-457, June 06-08, 1983
• 43: WOLPER, P. 1985. The tableau method for temporal logic: An overview. Logique et Analyse, Novelle Sdrie 28e Annde, 110-111 Numero Special. Automated Reasoning in Non-Classical Logic (June-Sept.), 119-136.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured); Tools
        D.2.10 Design**
            Subjects: Methodologies**; Representation**
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving
      F.4.3 Formal Languages
          Subjects: Decision problems

General Terms:
Design, Verification

Keywords:
automated deduction, concurrent systems, formal specification and verification, graphical user interface, real-time systems, temporal logic