Compositional Semantics and Refinement of Statecharts
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [34]
  • |
  • Related
  • |
  • Cited by [4]
  • | |
  • Comments
    Abstract:

    Statecharts is widely used as a behavioral modeling language for reactive systems for its concise and intuitive expression. It can represent the system behavior at different levels of abstraction, and therefore can represent the result of every refinement step in the process of system modeling. However, it’s beyond its capability to reason about whether the model semantics of the lower level preserves that of the higher level and whether the models they describe satisfy some properties. In this aspect, the formal language XYZ/E can be used complementarily. The XYZ/E is an executable linear temporal logic. It can express both the properties and behavior of systems. In this paper, the semantics of Statecharts is defined inductively using the Basic Transition System, and its temporal semantics is expressed by an XYZ/E formula. The semantics we give is modularly compositional. The semantic preserving of different refinement steps can be guaranteed by the semantic definition directly. Models that Statecharts specify and their properties are represented in the same logic, so the assertion that a model meets its specification is expressed by logical implication.

    Reference
    [1]Harel D.Statecharts:A visual formalism for complex systems.Science of Computer Programming,1987,8(3):231-274.
    [2]Manna Z,Pnueli A.The Temporal Logic of Reactive and Concurrent System:Specification.New York:Springer-Verlag,1992.
    [3]Tang ZS,et al.Temporal Logic Programming and Software Engineering.Beijing:Science Press,2002 (in Chinese).
    [4]Kesten Y,Manna Z,Pnueli A.Temporal verification of simulation and refinement.In:de Bakker JW,de Roever WP,Rozenberg G,eds.Proc.of the Decade of Concurrency.LNCS 803,Berlin:Springer-Verlag,1994.273-346.
    [5]Zhu XY,Tang ZS.A temporal logic-based software architecture description language XYZ/ADL.Journal of Software,2003,14(4):713-720 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/14/713.htm
    [6]Zhu XY,Tang ZS.A temporal logic semantics for UML activity diagrams.Journal of Computer Research and Development,2005,42(9):1478-1484 (in Chinese with English abstract).
    [7]Harel D,Pnueli A,Schmidt JP,Sherman R.On the formal semantics of Statecharts.In:Pnueli A,ed.Proc.of the 2nd IEEE Symp.on Logic in Computer Science.Washington:Computer Society Press of the IEEE,1987.56-64.
    [8]Pnueli A,Shalev M.What is in a step:On the semantics of Statecharts.In:Ito T,Mayer AR,eds.Proc.of the Symp.on Theoretical Aspects of Computer Science.LNCS 526,Berlin:Springer-Verlag,1991.244-264.
    [9]Harel D,Naamad A.The STATEMATE semantics of Statecharts.ACM Trans.on Software Engineering and Methodology,1996,5(4):293-333.
    [10]Leveson NG,Heimdahl MPE,Hildreth H,Reese JD.Requirements specification for process-control systems.IEEE Trans.on Software Engneering,1994,20(9):684-707.
    [11]Hooman JJM,Ramesh S,de Roever WP.A compositional axiomatization of Statecharts.Theoretical Computer Science,1992,101(2):289-335.
    [12]Uselton A,Smolka SA.A compositional semantics for Statecharts using labeled transition systems.In:Jonsson B,Parrow J,eds.Proc.of the 5th Int'l Conf.on Concurrency Theory.LNCS 836,Berlin:Springer-Verlag,1994.2-17.
    [13]Uselton A,Smolka SA.A process algebraic semantics for Statecharts via state refinement.In:Olderog ER,ed.Proc.of the IFIP Working Conf.on Programming Concepts,Methods and Calculi.North-Holland:Elsevier Science Publishers,1994.
    [14]Huizing C,Gerth R,de Roever WP.Modeling Statecharts behavior in a fully abstract way.In:Dauchet M,Nivat M,eds.Proc.of the 13th Colloquium on Trees in Algebra and Programming.LNCS 299,Berlin:Springer-Verlag,1988.271-294.
    [15]Huizing C,de Roever WP.Introduction to design choices in the semantics of Statecharts.Information Processing Letters,1991,(37):205-213.
    [16]Maggiolo-Schettini A,Peron A,Tini S.Equivalences of Statecharts.In:Sassone M,ed.Proc.of the Concurrency Theory:the 7th Int'l Conf.LNCS 1119,Berlin:Springer-Verlag,1996.687-702.
    [17]Mikk E,Lakhnech Y,Siegel M.Hierarchical automata as model for Statecharts.In:Shyamasundar R,Euda K,eds.Proc.of the 3rd Asian Computing Science Conf.LNCS 1345,Berlin:Springer-Verlag,1997.181-196.
    [18]von der Beeck M.A concise compositional Statecharts semantics definition.In:Bolognesi T,Latella D,eds.Proc.of the Formal Techniques for Distributed System Development,FORTE/PSTV 2000.Boston:Kluwer Academic Publishers,2000.
    [19]Lüttgen G,von der Beeck M,Cleaveland R.A compositional approach to Statecharts semantics.In:Rosenblum DS,ed.Proc.of the 8th Foundations of Software Engineering (FSE-8).New York:ACM Press,2000.120-129.
    [20]Mikk E,Lakhnech Y,Petersohn C,Siegel M.On formal semantics of Statecharts as supported by STATEMATE.In:Duke DJ,Evans AS,eds.Proc.of the 2nd BCS-FACS Northern Formal Methods Workshop.Berlin:Springer-Verlag,1997.
    [21]Lüttgen G,vonder Beeck M,Cleaveland R.Statecharts via process algebra.In:Baeten JCM,Mauw S,eds.Proc.of the Concurrency Theory,10th Int'l Conf.LNCS 1664,Berlin:Springer-Verlag,1999.399-414.
    [22]Lüttgen G,Mender M.The intuitionism behind Statecharts steps.ACM Trans.on Computational Logic,2002,3(1):1-38.
    [23]von der Beeck M.A comparision of Statechart variants.In:de Roever WP,Langmaack H,Vytopil J,eds.Proc.of the Formal Techniques in Real-Time and Fault-Tolerant Systems.LNCS 863,Berlin:Springer-Verlag,1994.128-148.
    [24]Latella D,Majzik I,Massink M.Towards a formal operational semantics of UML Statechart diagrams.In:Ciancarini P,Fantechi A,Gorrieri R,eds.Proc.of the 3rd Int'l Conf.on Formal Methods for Open Object-Oriented Distributed Systems.Boston:Kluwer Academic Publishers,1999.15-18.
    [25]von der Beeck M.Formalization of UML-Statecharts.In:Gogolla M,Kobryn C,eds.Proc.of the Unified Modeling Language,Modeling Languages,Concepts,and Tools,4th Int'l Conf.LNCS 2185,Berlin:Springer-Verlag,2001.406-421.
    [26]Jiang H,Lin D,Xie XR.The formal semantics of UML state machine.Journal of Software,2002,13(12):2244-2250 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/13/2244.pdf
    [27]Dong W,Wang J,Qi ZC.An approach of model checking UML Statecharts.Journal of Software,2003,14(4):750-756 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/14/750.htm
    [28]Mikk E,Lakhnech Y,Siegel M.Towards efficient modelchecking Statecharts:A Statecharts to promela complier.In:Langerak R,ed.Proc.of the 3rd Int'l SPIN Workshop.LNCS 1516,Berlin:Springer-Verlag,1997.
    [29]Sowmya A,Ramesh S.Extending Statecharts with temporal logic.IEEE Trans.on Software Engineering,1998,24(3):216-231.
    [3]唐稚松,等.时序逻辑程序设计与软件工程.北京:科学出版社,2002.
    [5]朱雪阳,唐稚松.基于时序逻辑的软件体系结构描述语言XYZ/ADL.软件学报,2003,14(4):713-720.http://www.jos.org.cn/1000-9825/14/713.htm
    [6]朱雪阳,唐稚松.UML活动图的时序逻辑语义.计算机研究与发展,2005,42(9):1478-1484.
    [26]蒋慧,林东,谢希仁.UML状态机的形式语义.软件学报,2002,13(12):2244-2250.http://www.jos.org.cn/1000-9825/13/2244.pdf
    [27]董威,王戟,齐治昌.UML Statecharts的模型检验方法.软件学报,2003,14(4):750-756.http://www.jos.org.cn/1000-9825/14/750.htm
    Related
    Comments
    Comments
    分享到微博
    Submit
Get Citation

朱雪阳,唐稚松. Statecharts的组合语义与求精.软件学报,2006,17(4):670-681

Copy
Share
Article Metrics
  • Abstract:4782
  • PDF: 5911
  • HTML: 0
  • Cited by: 0
History
  • Received:July 29,2004
  • Revised:October 20,2005
You are the first2032778Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063