A model parametric real-time logic

ABSTRACT

TRIO is a formal notation for the logic-based specification of real-time systems. In this paper the language and its straightforward model-theoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with reference to a variety of underlying time structures such as infinite-time structures (both dense and discrete) and finite-time structures. The main motivation is the ability to validate formal specifications. A solution to this problem is presented, which gives a new, model-parametric semantics to the language. An algorithm for constructively verifying the satisfiability of formulas in the decidable cases is defined, and several important temporal properties of specifications are characterized.

REFERENCES

• 1: Peter B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press Professional, Inc., San Diego, CA, 1986
• 2: ATTIYA, H., AND LYNCH, N.A. Time bounds for real-tlme process control in the presence of timing uncertainty. In IEEE Symposzum on Real-Time Systems. IEEE, New York, 1989.
• 3: BARRINGER, H., CHENG, J. H., AND JONES, C.B. A logic covering undefinedness in program proofs. Acta Inf 21 1984, 251-269.
• 4: BEN-ARL M., PNUELI, A., AND MANNA, Z. The temporal logic of branching t~me. Acta Inf 20 (1983), 207-226.
• 5: Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, Proceedings of the eighth ACM symposium on Operating systems principles, p.1-11, December 14-16, 1981, Pacific Grove, California, United States
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: COEN, A., MORZENTI, A., AND SCIUTO, D. Specification and verlfication of hardware systema using the temporal logic language TRIO. In Proeeedings oflFOP lOth International Conference on Hardware Descrtptwn Languages and Thezr Applieatzons, D. Borrione and R. Waxman, Eds., North-Holland, Amsterdam, 1991, pp. 43-61.
• 8: N. Gehani, Ada: an advanced introduction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1983
• 9: GHEZZI, C., MANDRIOLI, D., AND MORZENTI, A. TRIO, a logic language for executable specifications of real-time systems. In Proceedings of lOth Fr~neh-Tunisian Semmar on Computer Science. (Tunls, May 1989), pp. 322-349.
• 10: 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]
• 11: GUTTAG, J. V., HOROWITZ, E., MUSSER, D. The design of data type specifications. In Current Trends ~n Programm~ng Methodologies, vol. 4, R. T. Yeh, Ed. Prentice-Hall, Englewood Cliffs, N.J., 1978.
• 12: 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
• 13: KEMMERER, R.A. Testing software specifications to detect design errors. Trans. Softw. Eng. 11, 1 (Jan. 1985), 32-43.
• 14: KOYMANS, R. Specifying message passing and time-critical systems with temporal togic. Ph.D. dissertation, Eindhoven Univ. of Technology, The Netherlands, 1989.
• 15: Ron Koymans , Willem P. de Roever, Examples of a Real-Time Temporal Logic Specification, The Analysis of Concurrent Systems, p.231-251, September 12-16, 1983
• 16: KOYMANS, R., KUIPER, R., AND ZIJLSTRA, E. Specifying message passing and real-time systems with real-time temporal logic. In ESPRIT '87 Achievement and Impact. North-Holland, Amsterdam, 1987, pp. 311-324.
• 17: Fred Kröger, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1987
• 18: Nancy Lynch , Hagit Attiya, Using mappings to prove timing properties, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.265-280, August 22-24, 1990, Quebec City, Quebec, Canada [doi>10.1145/93385.93428]
• 19: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 20: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 21: MORZENTI, A. The specification of real-time systems: Proposal of a logical formalism. Ph.D. dissertation, Dipartimento di Elettronica, Politecnico di Milano, Italy, 1989 (in Italian).
• 22: MOeZENTI, A., AND SAN PIETRO, P. TRIO specification of maneuvre regulation in pondage power stations. ENEL-CRA Res. Rep., Politecnico di Milano, Italy, June 1990 (in Italian).
• 23: MORZENTI, A., RATTO, E., RONCATO, M., AND ZOCCOLANTE, L. TRIO, a logic formalism for the specification ofreal-time systems. In Proceedings of lEEE Euromicro Workshop on Real-Time. IEEE, New York, 1989, pp. 26-30.
• 24: MOSZKOWSKI, B. A temporal logic for multilevel reasoning about hardware. Computer 18, (Feb. 1985), 10-19.
• 25: NARAYANA, K. T., AND AABY, A.A. Specification of real-time systems in real-time temporal interval log~c. In Proceedings of lEEE Symposium on Real-Time Systems. IEEE, New York, 1988, pp. 86-95.
• 26: OSTROFF, J.S. Modelling, specifying and verifying real-time embedded computer systems. In Procee&ngs of IEEE Symposium on Real-Time Systems. IEEE, New York, 1987, pp. 124-132.
• 27: Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
• 28: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 29: PNUELI, A. The Temporal Semantics of Concurrent Programs. Theoretical Computer Science, vol. 13. North-Holland, Amsterdam, 1981, pp. 45-60.
• 30: RESCHER, N., AND URQUHART, A. Temporal Logic. Springer-Verlag, New York, 1971.
• 31: 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
• 32: SMULLIAN, R.M. First Order Logic. Springer-Verlag, New York, 1968.
• 33: Niklaus Wirth, Toward a discipline of real-time programming, Communications of the ACM, v.20 n.8, p.577-583, Aug. 1977 [doi>10.1145/359763.359798]
• 34: WOLPER, P. Temporal logic can be more expressive, lnf. Control 56 (1983), 72-99.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools
  D.4 OPERATING SYSTEMS
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Model theory

General Terms:
Languages

Keywords:
first-order logic, formal specifications, model-theoretic semantics, real-time systems, requirements validation, temporal logic