
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Riccardo Mattolini, Paolo Nesi, "An Interval Logic for RealTime System Specification," IEEE Transactions on Software Engineering, vol. 27, no. 3, pp. 208227, March, 2001.  
BibTex  x  
@article{ 10.1109/32.910858, author = {Riccardo Mattolini and Paolo Nesi}, title = {An Interval Logic for RealTime System Specification}, journal ={IEEE Transactions on Software Engineering}, volume = {27}, number = {3}, issn = {00985589}, year = {2001}, pages = {208227}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.910858}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  An Interval Logic for RealTime System Specification IS  3 SN  00985589 SP208 EP227 EPD  208227 A1  Riccardo Mattolini, A1  Paolo Nesi, PY  2001 KW  Formal specification language KW  first order logic KW  temporal interval logic KW  verification and validation KW  realtime systems. VL  27 JA  IEEE Transactions on Software Engineering ER   
Abstract—Formal techniques for the specification of realtime 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 TemporalInterval Logic with Compositional Operators (TILCO) designed expressly for the specification of realtime systems. TILCO is a generalization of classical temporal logics based on the operators
[1] G. Bucci, M. Campanai, and P. Nesi, "Tools for Specifying RealTime Systems," J. RealTime Systems, Mar. 1995, pp. 117172.
[2] A.D. Stoyenko, “The Evolution and StateoftheArt of RealTime 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 realtime systems,”IEEE Trans. Software Eng., vol. SE12, pp. 890–904, Sept. 1986.
[5] R.L. Schwartz, P.M. MelliarSmith, and F.H. Vogt, “A Interval Logic for HigherLevel 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 ObjectOriented Extension to Z,” Proc. Fourth Ann. Z User Meeting, Workshop in Computing, J.E. Nicholls, ed., pp.151172, 1991.
[10] K. Lano and H. Haughton, eds., ObjectOriented Specification Case Studies.Englewood Cliffs, N.J.: Prentice Hall, 1993.
[11] D. Carrington, D. Duke, R. Duke, P. King, G. Rose, and G. Smith, “ObjectZ: An ObjectOriented 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 ObjectOriented Designs,” Proc. Int'l Conf. Technology of ObjectOriented Languages and Systems, TOOLS 7, G. Heeg, B. Mugnusson, and B. Meyer, eds., pp. 6378, 1992.
[13] J. Ostroff, "Formal Methods for the Specification and Design of RealTime Safety Critical Systems," J. Systems Software, vol. 18, no. 1, 1992.
[14] M. BenAri, 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 RealTime 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 RealTime Systems," J. Systems and Software, vol. 12, no. 2, pp. 107123, May 1990.
[19] R. Koymans, Specifying Message Passing and TimeCritical Systems with Temporal Logic, Lecture Notes in Computer Science 651, SpringerVerlag, 1992.
[20] R. Koymans, “Specifying RealTime Properties with Metric Temporal Logic,” J. RealTimeSystems, vol. 2, no. 4, pp. 255299, Nov. 1990.
[21] J.F. Allen and G. Ferguson, “Actions and Events in Interval Temporal Logic,” Technical Report TRURCSD 521, Univ. of Rochester, Computer Science Dept., Rochester, New York, July 1994.
[22] R. Alur and T.A. Henzinger, RealTime Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390401, 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. MelliarSmith, “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 realtime programs,” Proc. ACMSIGSOFT Conf., 1989.
[31] L.K. Dillon, G. Kutty, L.E. Moser, P.M. MelliarSmith, and Y.S. Ramakrishna, “A Graphical Interval Logic for Specifying Concurrent Systems,” ACM Trans. Software Eng. Methods, vol. 3, no. 2, pp. 131165, 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. 120.
[36] M. Felder and A. Morzenti, “Validating RealTime Systems by HistoryChecking TRIO Specifications,” Proc. 14th Int'l Conf. Software Eng., pp. 199–211, May 1992.
[37] J.S. Ostroff and W. Wonham, “Modeling and Verifying RealTime Embedded Computer Systems,” Proc. Eighth IEEE RealTime Systems Symp., pp. 124–132, Dec. 1987.
[38] G. Bucci, M. Campanai, P. Nesi, and M. Traversi, “An ObjectOriented 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 ObjectOriented 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 RealTime Systems," Proc. 18th Ann. ACM Symp. Principles of Programming Languages, pp. 353366, 1990.
[41] R. Alur and T.A. Henzinger, RealTime Logics: Complexity and Expressiveness Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 390401, 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 RealTime 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 RealTime Systems Through Logical Specifications and Petri Net Models,” Technical Report 91072, 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, “SuperExponential 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 ObjectLogics,” 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 DSIRT 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 DSIRT 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 RealTime Systems,” Technical Report 91072, Politecnico di Milano, Dipartimento di Elettronica e Informazione, Milano, Italy, 1992.
[62] M. Felder and A. Morzenti, “Validating RealTime Systems by HistoryChecking 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 LogicBased Languages,” Software Measurment, A. Melton, ed., pp. 93–113, 1996.
[65] S.N. Cant, D.R. Jeffery, and B. HendersonSellers, “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 ObjectOriented RealTime Systems Specification Languages," J. Systems and Software, Vol. 34, No. 1, 1996, pp. 4365.
[69] I. Suzuki,“Formal analysis of the alternating bit protocol by temporal Petrinets,” IEEE Transactions on Software Engineering, vol. 16, no. 11, Nov. 1990.