This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Interval Logic for Real-Time System Specification
March 2001 (vol. 27 no. 3)
pp. 208-227

Abstract—Formal techniques for the specification of real-time systems must be capable of describing system behavior as a set of relationships expressing the temporal constraints among events and actions, including properties of invariance, precedence, periodicity, liveness, and safety conditions. This paper describes a Temporal-Interval Logic with Compositional Operators (TILCO) designed expressly for the specification of real-time systems. TILCO is a generalization of classical temporal logics based on the operators eventually and henceforth; it allows both qualitative and quantitative specification of time relationships. TILCO is based on time intervals and can concisely express temporal constraints with time bounds, such as those needed to specify real-time systems. This approach can be used to verify the completeness and consistency of specifications, as well as to validate system behavior against its requirements and general properties. TILCO has been formalized by using the theorem prover Isabelle/HOL. TILCO specifications satisfying certain properties are executable by using a modified version of the Tableaux algorithm. This paper defines TILCO and its axiomatization, highlights the tools available for proving properties of specifications and for their execution, and provides an example of system specification and validation.

[1] G. Bucci, M. Campanai, and P. Nesi, "Tools for Specifying Real-Time Systems," J. Real-Time Systems, Mar. 1995, pp. 117-172.
[2] A.D. Stoyenko, “The Evolution and State-of-the-Art of Real-Time Languages,” J. Systems and Software, pp. 61–84, Apr. 1992.
[3] A. Pnueli, “The Temporal Logic of Programs,” Proc. 18th IEEE Foundations of Computer Science (FOCS), 1977.
[4] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[5] R.L. Schwartz, P.M. Melliar-Smith, and F.H. Vogt, “A Interval Logic for Higher-Level Temporal Reasoning,” Proc. Second Ann. ACM Symp. Principles of Distributed Computing, pp. 173–186, Aug. 1983.
[6] R. Gotzhein, “Temporal Logic and Applications—A Tutorial,” Computer Networks and ISDN Systems, vol. 24, pp. 203–218, 1992.
[7] L. Vila, “A Survey on Temporal Reasoning in Artificial Intelligence,” AI Comm., vol. 7, pp. 4–28, Mar. 1994.
[8] P. Zave, “An Operational Approach to Requirements Specification for Embedded Systems,” IEEE Trans. Software Eng., vol. 8, pp. 250–269, May 1982.
[9] K. Lano, “Z++, an Object-Oriented Extension to Z,” Proc. Fourth Ann. Z User Meeting, Workshop in Computing, J.E. Nicholls, ed., pp.151-172, 1991.
[10] K. Lano and H. Haughton, eds., Object-Oriented Specification Case Studies.Englewood Cliffs, N.J.: Prentice Hall, 1993.
[11] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G. Smith, “Object-Z: An Object-Oriented Extension to Z,” Formal Description Techniques, S.T. Voung, ed., 1990.
[12] E.H.H. Dürr and J. van Katwiik, “VDM++: A Formal Specification Language for Object-Oriented Designs,” Proc. Int'l Conf. Technology of Object-Oriented Languages and Systems, TOOLS 7, G. Heeg, B. Mugnusson, and B. Meyer, eds., pp. 63-78, 1992.
[13] J. Ostroff, "Formal Methods for the Specification and Design of Real-Time Safety Critical Systems," J. Systems Software, vol. 18, no. 1, 1992.
[14] M. Ben-Ari, Mathematical Logic for Computer Science. New York: Prentice Hall, 1993.
[15] R. Alur and T.A. Henzinger, “A Really Temporal Logic,” Proc. 30th IEEE Foundations of Computer Science (FOCS), 1989.
[16] J. Ostroff, Temporal Logic for Real-Time Systems. John Wiley and Sons, 1989.
[17] B.C. Moszkowski, “Executing Temporal Logic Programs,” PhD thesis, Cambridge Univ., 1986.
[18] C. Ghezzi, D. Mandriolli, and A. Morzenti, "Trio: A Logic Language for Executable Specifications of Real-Time Systems," J. Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
[19] R. Koymans, Specifying Message Passing and Time-Critical Systems with Temporal Logic, Lecture Notes in Computer Science 651, Springer-Verlag, 1992.
[20] R. Koymans, “Specifying Real-Time Properties with Metric Temporal Logic,” J. Real-Time-Systems, vol. 2, no. 4, pp. 255-299, Nov. 1990.
[21] J.F. Allen and G. Ferguson, “Actions and Events in Interval Temporal Logic,” Technical Report TR-URCSD 521, Univ. of Rochester, Computer Science Dept., Rochester, New York, July 1994.
[22] R. Alur and T.A. Henzinger, Real-Time Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390-401, 1990.
[23] Z. Manna and A. Pnueli, “Proving Precedence Properties: The Temporal Way,” Proc. 10th Colloquium on Automata Languages and Programming, J. Diaz, ed., pp. 491–512, July 1983.
[24] R. Rosner and A. Pnueli, “A Choppy Logic,” Proc. First IEEE Symp. Logic in Computer Science, pp. 306–313, 1986.
[25] R.L. Schwartz and P.M. Melliar-Smith, “From State Machines to Temporal Logic: Specification Methods for Protocol Standards,” IEEE Trans. Comm., vol. 30, pp. 2486–2496, Dec. 1982.
[26] J. Halpern, Z. Manna, and B. Moszkowski, “A Hardware Semantics Based on Temporal Intervals,” Proc. 10th Colloquium on Automata Languages and Programming, J. Diaz, ed., pp. 278–291, July 1983.
[27] J.Y. Halpern and Y. Shoham, “A Propositional Modal Logic of Time Intervals,” Proc. First IEEE Symp. Logic in Computer Science, pp. 274–292, 1986.
[28] P. Ladkin, “Models of Axioms for Time Intervals,” Proc. Sixth Nat'l Conf. Artificial Intelligence (AAAI '87), pp. 234–239, 1987.
[29] P.M. MelliarSmith, “Extending Interval Logic to Real Time Systems,” Proc. Temporal Logic Specification United Kingdom, B. Banieqbal, H. Barringer, and A. Pnueli, eds., pp. 224–242, Apr. 1987.
[30] R.R. Razouk and M.M. Gorlik,“A real time interval logic for reasoning about executions of real-time programs,” Proc. ACM-SIGSOFT Conf., 1989.
[31] L.K. Dillon, G. Kutty, L.E. Moser, P.M. Melliar-Smith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131-165, Apr. 1994.
[32] J.F. Allen, “Maintaining Knowledge about Temporal Intervals,” Comm. ACM, vol. 26, no. 11, pp. 832–843, 1983.
[33] E.A. Emerson and J.Y. Halpern, “Sometimes and Not Never Revisited: On Branching Versus Linear Time Temporal Logic,” J. the ACM, vol. 33, pp. 151–178, Jan. 1986.
[34] C. Stirling, “Comparing Linear and Branching Time Temporal Logics,” Proc. Int'l Conf. Temporal Logic in Specification, B. Banieqbal, H. Barringer, and P. Pnueli, eds., pp. 1–20, Apr. 1987.
[35] J. Fisher, "Roadmapping the High Density PWBs," Proc. IPC National Conf.: Solutions for Ultra High Density PWBs, Institute for Interconnecting and Packaging Electronic Circuits, Northbrook, Il., 1996, pp. 1-20.
[36] M. Felder and A. Morzenti, “Validating Real-Time Systems by History-Checking TRIO Specifications,” Proc. 14th Int'l Conf. Software Eng., pp. 199–211, May 1992.
[37] J.S. Ostroff and W. Wonham, “Modeling and Verifying Real-Time Embedded Computer Systems,” Proc. Eighth IEEE Real-Time Systems Symp., pp. 124–132, Dec. 1987.
[38] G. Bucci, M. Campanai, P. Nesi, and M. Traversi, “An Object-Oriented Dual Language for Specifying Reactive Systems,” Proc. IEEE Int'l Conf. Requirements Eng. (ICRE '94), Apr. 1994
[39] G. Bucci, M. Campanai, P. Nesi, and M. Traversi, “An Object-Oriented CASE Tool for Reactive System Specification,” Proc. Sixth Int'l Conf. Software Eng. and Its Applications, Nov. 1993
[40] T.A. Henzinger, Z. Manna, and A. Pnueli, "Temporal Proof Methodologies for Real-Time Systems," Proc. 18th Ann. ACM Symp. Principles of Programming Languages, pp. 353-366, 1990.
[41] R. Alur and T.A. Henzinger, Real-Time Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390-401, 1990.
[42] L.C. Paulson, “Isabelle: A Generic Theorem Prover,” Lecture Notes in Computer Science, Springer Verlag, 1994.
[43] R. Mattolini, “TILCO: A Temporal Logic for the Specification of Real-Time Systems (TILCO: una Logica Temporale per la Specifica di Sistemi di Tempo Reale),” PhD thesis, Dipartimento di Sistemi e Informatica, Univ. of Florence, Italy, 1996.
[44] M. Felder, D. Mandrioli, and A. Morzenti, “Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models,” Technical Report 91-072, Politecnico di Milano, Dipartimento di Elettronica e Informazione, 1991.
[45] R.E. Davis, Truth, Deduction, and Computation: Logic and Semantics for Computer Science. New York: Computer Science Press, 1989.
[46] J. Thistle and W.M. Wonham, “Control Problems in a Temporal Logic Framework,” Int'l J. Control, vol. 44, no. 4, 1986.
[47] H.B. Henderton, A Mathematical Introduction to Logic. New York: Academic Press, 1972.
[48] D.C. Cooper, “Theorem Proving in Arithmetic without Multiplication,” Machine Intelligence, American Elsevier, vol. 7, pp. 91–99, 1972.
[49] W.W. Bledsoe, “A New Method for Proving Certain Presburger Formulas,” Proc. Fourth Int'l Joint Conf. Artificial Intelligence, pp. 15–21, Sept. 1975.
[50] M.J. Fischer and M.O. Rabin, “Super-Exponential Complexity of Presburger Arithmentic,” Complexity of Computation, R.M. Karp, ed., pp. 27–31, 1974.
[51] R.E. Shostak, “A Practical Decision Procedure for Arithmetic with Function Symbols,” J. ACM, vol. 26, pp. 351–360, Apr. 1979.
[52] L.C. Paulson, “Isabelle: The Next 700 Theorem Provers,” Logic and Computer Science, P. Ochifreddi, ed., pp. 361–386, 1990.
[53] L.C. Paulson, ML for the Working Programmer. Cambridge Univ. Press, 1991.
[54] L.C. Paulson, “Isabelle's Object-Logics,” Technical Report 286, Computer Laboratory, Univ. of Cambridge, UK, 1994.
[55] A. Church, “A Formulation of the Simple Theory of Types,” J. Symbolic Logic, no. 5, pp. 56–68, 1940.
[56] J.P. Bowen and M.J.C. Gordon, “Z and HOL,” Z User Workshop, J.P. Bowen and J.A. Hall, eds., pp. 141–167, 1994.
[57] J.P. Bowen and M.J.C. Gordon, “A Shallow Embedding of Z in HOL,” Information and Software Technology, vol. 37, pp. 269–276, May/June 1995.
[58] J. Harrison, “Constructing the Real Numbers in HOL,” Technical Report HOL CB2 3QG, Univ. of Cambridge Computer Laboratory New Museums Site, Cambridge, England, 1993.
[59] R. Mattolini and P. Nesi, “Formalizing the Integers in Isabelle/HOL,” Technical Report DSI-RT 28/94, Dipartimento di Sistemi e Informatica, Universitádegli Studi di Firenze, 1994.
[60] A. Giotti, R. Mattolini, and P. Nesi, “Executing TILCO Specification with Tableaux,” Technical Report DSI-RT 31/95, Dipartimento di Sistemi e Informatica, Universitádegli Studi di Firenze, 1995.
[61] D. Mandrioli, S. Morasca, and A. Morzenti, “Functional Test Case Generation for Real-Time Systems,” Technical Report 91-072, Politecnico di Milano, Dipartimento di Elettronica e Informazione, Milano, Italy, 1992.
[62] M. Felder and A. Morzenti, “Validating Real-Time Systems by History-Checking TRIO Specifications,” ACM Trans. Software Eng. and Methodologies, vol. 3, no. 4, Oct. 1994.
[63] H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens, “METATEM: A Framework for Programming in Temporal Logic,” Proc. REX Workshop Stepwise Refinement of Distributed Systems: Models Formalism, Correctness, June 1989.
[64] R.A. McCauley and W.R. Edwards, “Analysis and Measurement Techniques for Logic-Based Languages,” Software Measurment, A. Melton, ed., pp. 93–113, 1996.
[65] S.N. Cant, D.R. Jeffery, and B. Henderson-Sellers, “A Conceptual Model of Cognitive Complexity of Elements of the Programming Process,” technical report, Univ. of New South Wales, Information Technology Research Centre, Australia, Oct. 1991.
[66] H. Zuse,Software Complexity.Berlin: Walter de Gruyter, 1991.
[67] S.D. Conte, H. E. Dunsmore, and V. Y. Shen, Software Engineering Metrics and Models, Benjamin/Cummings, Menlo Park, Calif., 1986.
[68] P. Nesi and M. Campanai, "Metric Framework for Object-Oriented Real-Time Systems Specification Languages," J. Systems and Software, Vol. 34, No. 1, 1996, pp. 43-65.
[69] I. Suzuki,“Formal analysis of the alternating bit protocol by temporal Petrinets,” IEEE Transactions on Software Engineering, vol. 16, no. 11, Nov. 1990.

Index Terms:
Formal specification language, first order logic, temporal interval logic, verification and validation, real-time systems.
Citation:
Riccardo Mattolini, Paolo Nesi, "An Interval Logic for Real-Time System Specification," IEEE Transactions on Software Engineering, vol. 27, no. 3, pp. 208-227, March 2001, doi:10.1109/32.910858
Usage of this product signifies your acceptance of the Terms of Use.