This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Extending Statecharts with Temporal Logic
March 1998 (vol. 24 no. 3)
pp. 216-231

Abstract—The task of designing large real-time reactive systems, which interact continuously with their environment and exhibit concurrency properties, is a challenging one. In this paper, we explore the utility of a combination of behavior and function specification languages in specifying such systems and verifying their properties. An existing specification language, statecharts, is used to specify the behavior of real-time reactive systems, while a new logic-based language called FNLOG (based on first-order predicate calculus and temporal logic, is designed to express the system functions over real time. Two types of system properties, intrinsic and structural, are proposed. It is shown that both types of system properties are expressible in FNLOG and may be verified by logical deduction, and also hold for the corresponding behavior specification.

[1] R. Koymans and R. Kuiper, "Paradigms for Real-Time Systems," Formal Techniques in Real-Time and Fault-Tolerant Systems, M. Joseph, ed., Lecture Notes in Computer Science 331, pp. 159-174. Springer-Verlag, 1988.
[2] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends," Current Trends in Concurrency, J. de Bakker et al., eds., Lecture Notes in Computer Science, vol. 224, Springer-Verlag, Berlin, 1986, pp. 510-584.
[3] R. Kurki-Suonio and T. Kankaanpaa, "On the Design of Reactive Systems," BIT, vol. 28, pp. 581-604, 1988.
[4] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[5] D.L. Parnas, "On the Use of Transition Diagrams in the Design of a User Interface for an Interactive Computer System," Proc. ACM Conf., pp. 379-385, 1969.
[6] R.J.K. Jacob, "Using Formal Specifications in the Design of a Human-Computer Interface," Comm. ACM, vol. 26, pp. 259-264, 1983.
[7] A.B. Ferrentino and H.D. Mills, "State Machines and Their Semantics in Software Engineering," Proc. IEEE COMPAS'77 Conf., pp. 242-251, 1977.
[8] M.D. Edwards and D. Aspinall, "The Synthesis of Digital Systems Using ASM Design Techniques," Computer Hardware Description Languages and Their Applications, Uehara and Barbacci, eds. NorthHolland, pp. 55-64, 1983.
[9] A.S. Tanenbaum, Computer Networks, third ed. Prentice Hall, 1996.
[10] C.A. Sunshine et al., "Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models," IEEE Trans. Software Eng., vol. 8, pp. 460-489, 1982.
[11] S. Feyock, "Transition-Based CAI/HELP Systems," Int'l J. Man-Machine Studies, vol. 9, pp. 399-413, 1977.
[12] CCITT (International Telecommunication Union), "Functional Specification and Description Language (SDL)," Recommendations Z.101-Z.104, vol. VI, Fasc. VI.7, Geneva, 1981.
[13] W.A. Woods, "Transition Network Grammars for Natural Language Analysis," Comm. ACM, vol. 13, no. 10, 1970, pp. 591-606.
[14] A. Wasserman, "Extending State Transition Diagrams for the Specification of Human-Computer Interaction," IEEE Trans. Software Eng., vol. 11, pp. 699-713, 1985.
[15] W. Reisig, “Petri Nets—An Introduction,” EATCS Monographs on Theoretical Computer Science. Springer-Verlag, vol. 4, 1985.
[16] R. Milner, A Calculus of Communicating Systems. Berlin: Springer Verlag, vol. 92, 1980.
[17] P. Zave, "A Distributed Alternative to Finite-State-Machine Specifications," ACM TOPLAS, vol. 7, no. 1, pp. 10-36, 1985.
[18] G. Berry and L. Cosserat, "The ESTEREL Synchronous Programming Language and Its Mathematical Semantics," Seminar Concurrency, S.D. Brookes, A.W. Roscoe, and G. Winskel, eds., Lecture Notes in Computer Science 197, pp. 389-448. Springer-Verlag, 1985.
[19] B.T. Hailpern,“Verifying concurrent processes using temporal logic,” Lecture Notes in Computer Science.New York: Springer-Verlag, 1982.
[20] R. Kuiper and W.P. de Roever, "Fairness Assumptions in CSP in a Temporal Logic Framework," Proc. IFIP Working Conf. Formal Descriptions of Programming Cconcepts II, pp. 127-134, 1982.
[21] L. Lamport, "Proving the Correctness of Multiprocess Programs," IEEE Trans. Software Eng., vol. 3, no. 2, pp. 125-143, 1977.
[22] L. Lamport, "What Good is Temporal Logic?" Proc. IFIP, pp. 657-668, NorthHolland, 1983.
[23] L. Lamport,“Specifying concurrent program modules,” ACM Trans. Programming Languages and Systems, vol. 5, no. 2, pp. 190-222, 1983.
[24] Z. Manna and A. Pnueli, "The Temporal Framework of Concurrent Programs," The Correctness Problem in Computer Science, R.S. Boyer and J.S. Moore, eds., pp. 215-274. Academic Press, 1981.
[25] Z. Manna and A. Pnueli, "How to Cook a Temporal Proof for Your Pet Language," Proc. 10th ACM POPL, 1983.
[26] Z. Manna and A. Pnueli, "Verification of Concurrent Programs: A Temporal Proof System," Foundations of Computer Science IV, J.W. de Bakker and J. Van Leeuwen, eds., Amsterdam: Mathematical Center Tracts 159, pp. 163-255, 1983.
[27] O. Lichtenstein, A. Pnueli, and L. Zuck, "The Glory of the Past," Logics of Programs, Lecture Notes in Computer Science, 1985.
[28] L. Lamport and S. Owicki, "Proving Liveness Properties of Concurrent Programs," ACM Trans. Programming Languages and Systems, vol. 4, pp. 455-495, July 1982.
[29] A. Pnueli, "The Temporal Logic of Programs," Proc. 18th Symp. Foundations of Computer Science, pp. 46-57, IEEE, 1977.
[30] A. Pnueli, "In Transition from Global to Modular Temporal Reasoning About Programs," Logic and Models of Concurrent Systems, K.R. Apt, ed., pp. 123-144. Springer-Verlag, 1985.
[31] A.P. Sistla and S.M. German, "Reasoning with Many Processes," Proc. Symp. Logic Computer Science,Ithaca, N.Y., pp. 138-152, IEEE, 1987.
[32] B.T. Hailpern,“Verifying concurrent processes using temporal logic,” Lecture Notes in Computer Science.New York: Springer-Verlag, 1982.
[33] B. Hailpern and S. Owicki, "Modular Verification of Computer Communication Protocols," IEEE Trans. Comm., vol. 31, no. 1, pp. 56-68, 1983.
[34] V. Nguyen, D. Gries, and S. Owicki, "A Model and Temporal Proof System for Network of Processes," Proc. 12th ACM Symp. Principles of Programming Languages, pp. 121-131, 1985.
[35] RL. Schwartz and P.M. Melliar-Smith, "From State Machines to Temporal Logic: Specification Methods for Protocol Standards," IEEE Trans. Comm., vol. 30, no. 12, pp. 2,486-2,496, 1982.
[36] S. Owicki and D. Gries, "An Axiomatic Proof Technique for Parallel Programs," Acta Informatica, vol. 6, pp. 319-340, 1976.
[37] E.M. Clarke, D.E. Long, and K.L. McMillan, “Compositional Model Checking,” Proc. Fourth Ann. Symp. Logic in Computer Science, June 1989.
[38] 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.
[39] R. Alur, C. Courcoubetis, and D. Dill, "Model-Checking for Probabilistic Real-Time Systems," Proc. ICALP, 1991.
[40] A. Pnueli and E. Harel, "Applications of Temporal Logic to the Specification of Real-Time Systems," Formal Techniques in Real-Time and Fault-Tolerant Systems, M. Joseph, ed., Lecture Notes in Computer Science 331, pp. 84-98. Springer-Verlag, 1988.
[41] Z. Manna and A. Pneuli, "Clocked Transition Systems," Technical Report STAN-CS-TR-96-1566, 1996.
[42] M.Y. Vardi and P. Wolper, "An Automata-Theoretic Approach to Automatic Program Verification," Proc. Symp. LICS,Cambridge, Mass., pp. 332-344, IEEE, 1986.
[43] M.C. Brown, "An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic," Proc. Symp. LICS,Cambridge, Mass., pp. 260-266, IEEE, 1986.
[44] J. Ostroff, "Formal Methods for the Specification and Design of Real-Time Safety Critical Systems," J. Systems Software, vol. 18, no. 1, 1992.
[45] J. Ostroff, "A Visual Toolset for the Design of Real-Time Discrete-Event Systems," IEEE Trans. Control Systems Technology, vol. 5, no. 3, pp. 320-337, May 1997.
[46] D.I. Good, R.M. Cohen, and J. Keeton-Williams, "Principles of Proving Concurrent Programs in Gypsy," Proc. Sixth ACM Symp. Principles of Programming Languages, 1979.
[47] P.M. Melliar-Smith and R.L. Schwartz, "Formal Specification and Mechanical Verification of SIFT: A Fault-Tolerant Flight Control System," IEEE Trans. Computing, vol. 31, no. 7, pp. 616-630, 1982.
[48] F. Cristian, "A Rigorous Approach to Fault-Tolerant System Development," IBM Resolution Report RJ 4008 (45056), 1983.
[49] M.P. Herlihy and J.M. Wing, "Specifying Graceful Degradation in Distributed Systems," Proc. Principles of Distributed Computing,Vancouver, Canada, 1987.
[50] I. Durham and M. Shaw, "Specifying Reliability as a Software Attribute," CMU Technical Report CS-82-148, Dec. 1982.
[51] J.M. Wing and M.R. Nixon, "Extending Ina Jo with Temporal Logic," IEEE Trans. Software Eng., vol. 15, no. 2, pp. 181-197, 1989.
[52] G.M. Karam and J.A. Buhr, "Temporal Logic-Based Deadlock Analysis for Ada," IEEE Trans. Software Eng., vol. 17, no. 10, pp. 1,109-1,125, 1991.
[53] J.S. Sagoo and D.J. Holding, "The Use of Temporal Petri Nets in the Specification and Design of Systems with Safety Implications," Algorithms and Architectures for Real-Time Control, P.J. Fleming and D.I. Jones, eds., IFAC Workshop Series, no. 4, pp. 231-236, Pergamon Press, 1992.
[54] J. Hooman, S. Ramesh, and W.P. De Roever, "A Compositional Semantics for Statecharts," Proc. Formal Models of Concurrency,Novosibirsk, USSR, 1989.
[55] J.J.M. Hooman, S. Ramesh, and W.P. de Roever, "A Compositional Axiomatization of Statecharts," Theoretical Computing Science, vol. 101, pp. 289-335, 1992.
[56] C. Huizing, R. Gerth, and W.P. De Roever, "Modelling Statecharts Behavior in a Fully Abstract Way," M. Dauchet and M. Nivat, CAPP '88, Lecture Notes in Computer Science 299. Springer-Verlag, 1988.
[57] I.J. Cox and N.H. Gehani, "Concurrent Programming and Robotics," Int'l J. Robotics Resolution, vol. 8, no. 2, pp. 3-16, 1989.
[58] A. Sowmya, S. Ramesh, and J.R. Isaac, "A Statechart Approach to Specification and Verification of Autonomous Mobile Robot Behavior," Proc. Int'l Conf. Automation, Robotics and Computer Vision ICARC '90, pp. 499-503.Singapore: McGraw-Hill, 1990.
[59] B.J. Kuipers and T.S. Levitt, "Navigation and Mapping in Large-Scale Space," Artificial Information, vol. 9, no. 2, pp. 25-43, 1988.
[60] A. Sowmya and S. Ramesh, "Extending Statecharts with Temporal Logic," SCSE Report 9401, School of Computer Science and Eng., Univ. of New South Wales, 1994.
[61] A. Sowmya, "Autonomous Robot Motion: Specification and Verification," PhD thesis, Indian Inst. of Tech nology, Bombay, India, 1991.
[62] F. Kroger, "Temporal Logic of Programs," EATCS Monographs on Theoretical Computer Science, W. Brauer, G. Rozenberg, and A. Salomaa, eds. Springer-Verlag, 1987.
[63] A. Sowmya and S. Ramesh, "Verification of Timing Properties in a Statecharts-Based Model of Real-Time Reactive Systems," Distributed Computer Control Systems, IFAC Workshop Series 1992, no. 3, H. Kopetz and M.G. Rodd, eds. Pergamon Press, 1992.
[64] A. Sowmya and S. Ramesh, "A Semantics-Preserving Transformation of Statecharts to FNLOG," Proc. 14th IFAC Workshop Distributed Computer Control Systems,Seoul, Korea, 1997.

Index Terms:
Concurrency, FNLOG, formal specifications, reactive systems, real-time, robotics, statecharts, specification languages, state-machines, temporal logic.
Citation:
Arcot Sowmya, S. Ramesh, "Extending Statecharts with Temporal Logic," IEEE Transactions on Software Engineering, vol. 24, no. 3, pp. 216-231, March 1998, doi:10.1109/32.667880
Usage of this product signifies your acceptance of the Terms of Use.