
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Arcot Sowmya, S. Ramesh, "Extending Statecharts with Temporal Logic," IEEE Transactions on Software Engineering, vol. 24, no. 3, pp. 216231, March, 1998.  
BibTex  x  
@article{ 10.1109/32.667880, author = {Arcot Sowmya and S. Ramesh}, title = {Extending Statecharts with Temporal Logic}, journal ={IEEE Transactions on Software Engineering}, volume = {24}, number = {3}, issn = {00985589}, year = {1998}, pages = {216231}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.667880}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Extending Statecharts with Temporal Logic IS  3 SN  00985589 SP216 EP231 EPD  216231 A1  Arcot Sowmya, A1  S. Ramesh, PY  1998 KW  Concurrency KW  FNLOG KW  formal specifications KW  reactive systems KW  realtime KW  robotics KW  statecharts KW  specification languages KW  statemachines KW  temporal logic. VL  24 JA  IEEE Transactions on Software Engineering ER   
Abstract—The task of designing large realtime 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,
[1] R. Koymans and R. Kuiper, "Paradigms for RealTime Systems," Formal Techniques in RealTime and FaultTolerant Systems, M. Joseph, ed., Lecture Notes in Computer Science 331, pp. 159174. SpringerVerlag, 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, SpringerVerlag, Berlin, 1986, pp. 510584.
[3] R. KurkiSuonio and T. Kankaanpaa, "On the Design of Reactive Systems," BIT, vol. 28, pp. 581604, 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. 379385, 1969.
[6] R.J.K. Jacob, "Using Formal Specifications in the Design of a HumanComputer Interface," Comm. ACM, vol. 26, pp. 259264, 1983.
[7] A.B. Ferrentino and H.D. Mills, "State Machines and Their Semantics in Software Engineering," Proc. IEEE COMPAS'77 Conf., pp. 242251, 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. 5564, 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. 460489, 1982.
[11] S. Feyock, "TransitionBased CAI/HELP Systems," Int'l J. ManMachine Studies, vol. 9, pp. 399413, 1977.
[12] CCITT (International Telecommunication Union), "Functional Specification and Description Language (SDL)," Recommendations Z.101Z.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. 591606.
[14] A. Wasserman, "Extending State Transition Diagrams for the Specification of HumanComputer Interaction," IEEE Trans. Software Eng., vol. 11, pp. 699713, 1985.
[15] W. Reisig, “Petri Nets—An Introduction,” EATCS Monographs on Theoretical Computer Science. SpringerVerlag, vol. 4, 1985.
[16] R. Milner, A Calculus of Communicating Systems. Berlin: Springer Verlag, vol. 92, 1980.
[17] P. Zave, "A Distributed Alternative to FiniteStateMachine Specifications," ACM TOPLAS, vol. 7, no. 1, pp. 1036, 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. 389448. SpringerVerlag, 1985.
[19] B.T. Hailpern,“Verifying concurrent processes using temporal logic,” Lecture Notes in Computer Science.New York: SpringerVerlag, 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. 127134, 1982.
[21] L. Lamport, "Proving the Correctness of Multiprocess Programs," IEEE Trans. Software Eng., vol. 3, no. 2, pp. 125143, 1977.
[22] L. Lamport, "What Good is Temporal Logic?" Proc. IFIP, pp. 657668, NorthHolland, 1983.
[23] L. Lamport,“Specifying concurrent program modules,” ACM Trans. Programming Languages and Systems, vol. 5, no. 2, pp. 190222, 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. 215274. 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. 163255, 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. 455495, July 1982.
[29] A. Pnueli, "The Temporal Logic of Programs," Proc. 18th Symp. Foundations of Computer Science, pp. 4657, 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. 123144. SpringerVerlag, 1985.
[31] A.P. Sistla and S.M. German, "Reasoning with Many Processes," Proc. Symp. Logic Computer Science,Ithaca, N.Y., pp. 138152, IEEE, 1987.
[32] B.T. Hailpern,“Verifying concurrent processes using temporal logic,” Lecture Notes in Computer Science.New York: SpringerVerlag, 1982.
[33] B. Hailpern and S. Owicki, "Modular Verification of Computer Communication Protocols," IEEE Trans. Comm., vol. 31, no. 1, pp. 5668, 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. 121131, 1985.
[35] RL. Schwartz and P.M. MelliarSmith, "From State Machines to Temporal Logic: Specification Methods for Protocol Standards," IEEE Trans. Comm., vol. 30, no. 12, pp. 2,4862,496, 1982.
[36] S. Owicki and D. Gries, "An Axiomatic Proof Technique for Parallel Programs," Acta Informatica, vol. 6, pp. 319340, 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 RealTime Systems," Proc. 18th Ann. ACM Symp. Principles of Programming Languages, pp. 353366, 1990.
[39] R. Alur, C. Courcoubetis, and D. Dill, "ModelChecking for Probabilistic RealTime Systems," Proc. ICALP, 1991.
[40] A. Pnueli and E. Harel, "Applications of Temporal Logic to the Specification of RealTime Systems," Formal Techniques in RealTime and FaultTolerant Systems, M. Joseph, ed., Lecture Notes in Computer Science 331, pp. 8498. SpringerVerlag, 1988.
[41] Z. Manna and A. Pneuli, "Clocked Transition Systems," Technical Report STANCSTR961566, 1996.
[42] M.Y. Vardi and P. Wolper, "An AutomataTheoretic Approach to Automatic Program Verification," Proc. Symp. LICS,Cambridge, Mass., pp. 332344, 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. 260266, IEEE, 1986.
[44] J. Ostroff, "Formal Methods for the Specification and Design of RealTime Safety Critical Systems," J. Systems Software, vol. 18, no. 1, 1992.
[45] J. Ostroff, "A Visual Toolset for the Design of RealTime DiscreteEvent Systems," IEEE Trans. Control Systems Technology, vol. 5, no. 3, pp. 320337, May 1997.
[46] D.I. Good, R.M. Cohen, and J. KeetonWilliams, "Principles of Proving Concurrent Programs in Gypsy," Proc. Sixth ACM Symp. Principles of Programming Languages, 1979.
[47] P.M. MelliarSmith and R.L. Schwartz, "Formal Specification and Mechanical Verification of SIFT: A FaultTolerant Flight Control System," IEEE Trans. Computing, vol. 31, no. 7, pp. 616630, 1982.
[48] F. Cristian, "A Rigorous Approach to FaultTolerant 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 CS82148, 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. 181197, 1989.
[52] G.M. Karam and J.A. Buhr, "Temporal LogicBased Deadlock Analysis for Ada," IEEE Trans. Software Eng., vol. 17, no. 10, pp. 1,1091,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 RealTime Control, P.J. Fleming and D.I. Jones, eds., IFAC Workshop Series, no. 4, pp. 231236, 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. 289335, 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. SpringerVerlag, 1988.
[57] I.J. Cox and N.H. Gehani, "Concurrent Programming and Robotics," Int'l J. Robotics Resolution, vol. 8, no. 2, pp. 316, 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. 499503.Singapore: McGrawHill, 1990.
[59] B.J. Kuipers and T.S. Levitt, "Navigation and Mapping in LargeScale Space," Artificial Information, vol. 9, no. 2, pp. 2543, 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. SpringerVerlag, 1987.
[63] A. Sowmya and S. Ramesh, "Verification of Timing Properties in a StatechartsBased Model of RealTime 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 SemanticsPreserving Transformation of Statecharts to FNLOG," Proc. 14th IFAC Workshop Distributed Computer Control Systems,Seoul, Korea, 1997.