Temporal logics for real-time system specification

Abstract

The specification of reactive and real-time systems must be supported by formal, mathematically-founded methods in order to be satisfactory and reliable. Temporal logics have been used to this end for several years. Temporal logics allow the specification of system behavior in terms of logical formulas, including temporal constraints, events, and the relationships between the two. In the last ten years, temporal logics have reached a high degree of expressiveness. Most of the temporal logics proposed in the last few years can be used for specifying reactive systems, although not all are suitable for specifying real-time systems. In this paper we present a series of criteria for assessing the capabilities of temporal logics for the specification, validation, and verification of real-time systems. Among the criteria are the logic's expressiveness, the logic's order, presence of a metric for time, the type of temporal operators, the fundamental time entity, and the structure of time. We examine a selection of temporal logics proposed in the literature. To make the comparison clearer, a set of typical specifications is identified and used with most of the temporal logics considered, thus presenting the reader with a number of real examples.

References

1. ABRAMSKY, S. AND MAIBAUM, T. S. E., Eds. 1992. Handbook of Logic in Computer Science (vol. 1): Background: Mathematical Structures. Oxford University Press, Inc., New York, NY.
2. ALLEN, J. F. 1983. Maintaining knowledge about temporal intervals. Commun. ACM 26, 11 (Nov.), 832-843.
3. ALLEN, J. F. AND FERGUSON, G. 1994. Actions and events in interval temporal logic. Tech. Rep. TR-URCSD 521. University of Rochester, Rochester, NY.
4. ALUR, R. 1992. Logics and models of real time: A survey. Tech. Rep. Department of Computer Science, Cornell University, Ithaca, NY.
5. ALUR, R. AND HENZINGER, T.A. 1989. A really temporal logic. In Proceedings of the 30th IEEE Conference on Foundatiions of Computer Science, IEEE Computer Society Press, Los Alamitos, CA.
6. ALUR, R. AND HENZINGER, T.A. 1990. Real time logics: Complexity and expressiveness. In Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (LICS '90, June), IEEE Press, Piscataway, NJ, 390- 401.
7. ANDREWS, P.B. 1986. An Introduction to Mathematical Logic and Type Theory. Academic Press series in computer science and applied mathematics. Academic Press Prof., Inc., San Diego, CA.
8. ARMSTRONG, J. AND BARROCA, L. 1996. Specification and verification of reactive systern behavior: The railroad crossing example.qjReal-Time Syst. 10, 3, 143-178.
9. BARRINGER, H., FISHER, M., GABBAY, D., GOUGH, G., AND OWENS, R. 1990. METATEM: A framework for programming in temporal logic. In Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Mook, The Netherlands, May 29-June 2), J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 94-129.
10. BARRINGER, H., FISHER, M., GABBAY, D., AND HUNTER, A. 1991. Meta-reasoning in executable temporal logic. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, Morgan Kaufmann, San Mateo, CA.
11. BARRINGER, H., FISHER, M., GABBAY, D., OWENS, R., AND REYNOLDS, M., Eds. 1996. The Imperative Future: Principles of Executable Temporal Logic. Wiley Advanced software developmeAt series. John Wiley and Sons, Inc., New York, NY.
12. BEN-ARI, M. 1993. Mathematical Logic for Computer Science. Prentice-Hall International Series in Computer Science. Prentice- Hall, Inc., Upper Saddle River, NJ.
13. BEN-ARI, M., PNUELI, A., AND MANNA, Z. 1983. The temporal logic of branching time. Acta Inf. 20.
14. BuccI, G., CAMPANAI, M., AND NESI, P. 1995. Tools for specifying real-time systems. Real- Time Syst. 8, 2/3 (Mar./May 1995), 117-172.
15. CARRINGTON, D., DUKE, D., DUKE, R., KING, P., ROSE, G., AND SMITH, G. 1990. Object-Z: An object-oriented extension to Z. In Formal Description Techniques, S. T. Voung, Ed. Elsevier Science Inc., New York, NY.
16. CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (Apr. 1986), 244-263.
17. CLARKE, E. M. AND GRUMBERG, O. 1987. The model checking problem for concurrent systerns with many similar processes. In Proceedings of the International Conference on Temporal Logic in Specification (Altrincham, UK, Apr. 8-10), B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 188-201.
18. DAVIS, L. S., DEMENTHON, D., BESTUL, T., HAR- WOOD, D., SRINIVASAN, H. V., AND ZIAVRAS, S. 1989. RAMBO: Vision and planning on the connection machine. In Proceedings of the Sixth Scandanavian Conference on Image and Application (Oulu, Finland, June), 1-14.
19. DAVIS, R.E. 1989. Truth, Deduction, and Computation: Logic and Semantics for Computer Science. Computer Science Press, Inc., New York, NY.
20. DILLON, L. K., KUTTY, G., MOSER, L. E., MELLIAR- SMITH, P. M., AND RAMAKRISHNA, Y.S. 1994. A graphical interval logic for specifying concurrent systems. ACM Trans. Softw. Eng. Methodol. 3, 2 (Apr. 1994), 131-165.
21. D RR, E. AND VAN KATWIJK, J. 1992. VDM+ +: A formal specification language for object-oriented designs. In Proceedings of the Seventh International Conference on Technology of Object-Oriented Languages and Systems (TOOLS 7, Dortmund, Germany), G. Heeg, B. Magnusson, and B. Meyer, Eds. TOOLS conference series Prentice Hall International (UK) Ltd., Hertfordshire, UK, 63-78.
22. EMERSON, E. A. AND HALPERN, J. Y. 1986. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. J. ACM 33, 1 (Jan. 1986), 151-178.
23. EMERSON, E. A., MOK, A. K., SISTLA, A. P., AND SRINIVASAN, J. 1989. Quantitative temporal reasoning. In Proceedings of the Workshop on Finite-State Concurrency (Grenoble, France).
24. FELDER, M. AND MORZENTI, A. 1992. Validating real-time systems by history-checking TRIO specifications. In Proceedings of the 14th International Conference on Software Engineering (ICSE '92, Melbourne, Australia, May 11- 15), T. Montgomery, Ed. ACM Press, New York, NY, 199-211.
25. FELDER, M. AND MORZENTI, A. 1994. Validating real-time systems by history-checking TRIO specifications. ACM Trans. Softw. Eng. Methodol. 3, 4 (Oct. 1994), 308-339.
26. FINGER, M., FISHER, M., AND OWENS, R. 1993. Metamem at work: Modelling reactive systerns using executable temporal logic. In Proceedings of the 6th International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systerns (Edinburg, UK, June), Gordon and Breach Science Publishers, Inc., Langhorn, PA.
27. FISHER, M. AND OWENS, R. 1993. An introduction to executable modal and temporal logics. In Proceedings of the Workshop on Executable Modal and Temporal Logics (IJCAI '93, Chamberry, France, Aug.), M. Fisher and R. Owens, Eds. Springer-Verlag, New York.
28. GHEZZI, C., MANDRIOLI, D., AND MORZENTI, A. 1990. TRIO: A logic language for executable specifications of real-time systems. J. Syst. Softw. 12, 2 (May 1990), 107-123.
29. GOTZHEIN, R. 1992. Temporal logic and applications: a tutorial. Comput. Netw. ISDN Syst. 24, 3 (May 1, 1992), 203-218.
30. HALPERN, J., MANNA, Z., AND MOSZKOWSKI, B. 1983. A hardware semantics based on ternporal intervals. In Proceedings of the Tenth Colloquium on Automata Languages and Programming (Barcelona, Spain, July), J. Diaz, Ed. Springer-Verlag, New York.
31. HALPERN, J. Y. AND SHOHAM, Y. 1986. A propositional modal logic of time intervals. In Proceedings of the First IEEE Symposium on Logic in Computer Science, IEEE Press, Piscataway, NJ, 274-292.
32. HUGHES, G. E. AND CRESSWELL, M.K. 1968. An Introduction to Modal Logic. Muthuen and Co. Ltd., London, UK.
33. JAHANIAN, F AND MOK, A K 1986. Safety analysis of timing properties in real-time systems. IEEE Trans. Softw. Eng. SE-12, 9 (Sept. 1986), 890-904.
34. Joszo, B. 1987. MCTL: An extension of CTL for modular verification of concurrent systems. In Proceedings of the International Conference on Temporal Logic in Specification (Altrincham, UK, Apr. 8-10), B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer- Verlag, New York, NY, 165-187.
35. KOYMANS, R. 1990. Specifying real-time properties with metric temporal logic. Real-Time Syst. 2, 4 (Nov. 1990), 255-299.
36. LADKIN, P. 1987. Models of axioms for time intervals. In Proceedings of the Sixth National Conference on Artificial Intelligence (AAAI'87), AAAI Press, Menlo Park, CA, 234-239.
37. LANO, K. 1991.Z++, an object-oriented extension to z. In Proceedings of the Fourth Annual Meeting on Z User (Oxford, UK), J. E. Nicholls, Ed.Springer-Verlag, Secaucus, NJ, 151-172.
38. LANO, K. AND HAUGHTON, H., Eds. 1994. Object-Oriented Specification Case Studies. Prentice-Hall Object-Oriented Series. Prentice Hall International (UK) Ltd., Hertfordshire, UK.
39. MANNA, Z. AND PNUELI, A. 1983. Proving precedence properties: The temporal way. In Proceedings of the Tenth Colloquium on Automata Languages and Programming (Barcelona, Spain, July), J. Diaz, Ed. Springer-Verlag, New York, 491-512.
40. MANNA, Z. AND PNUELI, A. 1990. A hierarchy of temporal properties (invited paper). In Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing (PODC '90, Quebec City, Canada, Aug. 22- 24), C. Dwork, Ed. ACM Press, New York, NY, 377-410.
41. MATTOLINI, R. 1996. TILCO: A temporal logic for the specification of real-time systems (TILCO: una Logica Temporale per la Specifica di Sistemi di Tempo Reale). Ph.D. Dissertation.
42. MATTOLINI, R. AND NESI, P. 1996. Using Tilco for specifying real-time systems. In Proceedings of the Second IEEE International Conference on Engineering of Complex Computer Systems (Montreal, Canada), IEEE Computer Society Press, Los Alamitos, CA, 18-25.
43. MATTOLINI, R. AND NESI, P. 2000. An interval logic for real-time system specification (in press). IEEE Trans. Softw. Eng.
44. MELLIAR-SMITH, P.M. 1987. Extending interval logic to real time systems. In Proceedings of the Conference on Temporal Logic Specification (UK, Apr.), B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer-Verlag, New York, 224-242.
45. MERZ, S. 1993. Efficiently executable temporal logic programs. In Proceedings of the Workshop on Executable Modal and Temporal Logics (IJCAI '93, Chamberry, France, Aug.), M. Fisher and R. Owens, Eds. Springer-Verlag, New York, 1-20.
46. MOSER, L. E., RAMAKRISHNA, Y. S., KUTTY, G., MELLIAR-SMITH, P. M., AND DILLON, L. K. 1997. A graphical environment for the design of concurrent real-time systems. ACM Trans. Softw. Eng. Methodol. 6, 1, 31-79.
47. MOSZKOWSKI, B. 1985. A temporal logic for multilevel reasoning about hardware. IEEE Computer, 10-19.
48. MOSZKOWSKI, B. AND MANNA, Z. 1984. Reasoning in interval logic. In Proceedings of the ACM/NSF/ ONR Workshop on Logics of Programs, Springer-Verlag, Secaucus, NJ, 371-384.
49. MOSZKOWSKI, B. C. 1986. Executing temporal logic programs. Ph.D. Dissertation. Cambridge University Press, New York, NY.
50. ORGUN, M. AND MA, W. 1994. An overview of temporal logic programming. In Proceedings of the First International Conference on Ternporal Logic (ICTL, Bonn, Germany, July), Springer-Verlag, Secaucus, NJ.
51. OSTROFF, J. S. 1989. Temporal Logic for Real Time Systems. Wiley Advanced software development series. John Wiley and Sons, Inc., New York, NY.
52. OSTROFF, J.S. 1991. Verification of safety critical systems using ttm/rttl. In Proceedings of the REX Workshop on Real-Time: Theory in Practice, Springer-Verlag, New York, NY.
53. OSTROFF, J. S. 1992. Formal methods for the specification and design of real-time safety critical systems. J. Syst. Softw. 18, 1 (Apr. 1992), 33-60.
54. OSTROFF, J. S. AND WONHAM, W. 1987. Modeling and verifying real-time embedded computer systems. In Proceedings of the 8th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, Los Alamitos, CA, 124- 132.
55. OSTROFF, J. S. AND WONHAM, W. M. 1990. A framework for real-time discrete event control. IEEE Trans. Automat. Contr. 35, 4 (Apr.), 386 -397.
56. PAULSON, L.C. 1994. Isabelle: A Generic Theorein Prover. Lecture Notes in Computer Science, vol. 828. Springer-Verlag, New York, NY.
57. PNUELI, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press, Los Alamitos, CA, 46-57.
58. PNUELI, A. 1981. The temporal semantics of concurrent programs. Theor. Comput. Sci. 13.
59. PNUELI, A 1986. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current Trends in Concurrency. Overviews and Tutorials, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds. Springer Lecture Notes in Computer Science. Springer-Verlag, New York, NY, 510-584.
60. PRIOR, A. 1967. Past, Present and Future. Oxford University Press, Oxford, UK.
61. RAZOUK, R. AND GORLICK, M. 1989. Real-time interval logic for reasoning about executions of real-time programs. SIGSOFT Softw. Eng. Notes 14, 8 (Dec. 1989), 10-19.
62. ROSNER, R. AND PNUELI, A. 1986. A choppy logic. In Proceedings of the First IEEE Symposium on Logic in Computer Science, IEEE Press, Piscataway, NJ, 306-313.
63. SCHWARTZ, R. L. AND MELLIAR-SMITH, P.M. 1982. From state machines to temporal logic: Specification methods for protocol standards. IEEE Trans. Commun. 30, 12 (Dec.), 2486- 2496.
64. SCHWARTZ, R. L., MELLIAR-SMITH, P. M., AND VOGT, F.H. 1983. An interval logic for higherlevel temporal reasoning. In Proceedings of the Second ACM Symposium on Principles of Distributed Computing (Aug.), ACM Press, New York, NY, 173-186.
65. STANKOVIC, g. A. 1988. Misconceptions about real-time computing: a serious problem for next-generation systems. IEEE Computer 21, 10 (Oct. 1988), 10-19.
66. STANKOVIC, J. A. AND RAMAMRITHAM, K. 1990. What is predictability for real-time systems. IEEE Real-Time Syst. Newsl., 247-254.
67. STIRLING, C. 1987. Comparing linear and branching time temporal logics. In Proceedings of the International Conference on Ternporal Logic in Specification (Altrincham, UK, Apr. 8-10), B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Springer Lecture Notes in Computer Science Springer-Verlag, New York, NY, 1-20.
68. STOYENKO, A.D. 1992. The evolution and stateof-the-art of real-time languages. J. Syst. Softw. 18, 1 (Apr. 1992), 61-84.
69. VILA, L. 1994. A survey on temporal reasoning in artificial intelligence. AI Commun. 7, 1 (Mar. 1994), 4-28.
70. WANG, F., MOK, A. K., AND EMERSON, E. A. 1993. Distributed real-time system specification and verification in APTL. ACM Trans. Softw. Eng. Methodol. 2, 4 (Oct. 1993), 346-378.
71. ZAVE, P. 1982. An operational approach to requirements specification for embedded systerns. IEEE Trans. Softw. Eng. 8, 3 (May), 250 -269.

Index Terms

• Applied computing

  • Computers in other domains

• Computer systems organization

  • Real-time systems

• Computing methodologies

  • Artificial intelligence

    • Knowledge representation and reasoning

      • Temporal reasoning

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • System description languages

      • Specification languages

  • Software organization and properties

    • Software functional properties

      • Formal methods

• Theory of computation

  • Logic

    • Modal and temporal logics