Statecharts的组合语义与求精
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.60273025, 60223005 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2004AA1Z2100 (国家高技术研究发展计划(863)); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973))


Compositional Semantics and Refinement of Statecharts
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [34]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    由于简洁、直观的表达能力,Statecharts被用于许多反应系统的行为建模.Statecharts可表示不同抽象层次的系统行为,因而可用来表示逐步求精建模中各步的结果.但对于求精过程中下层是否保持了上层的语义、所建模型是否满足某些性质的问题,却难以在其自身的框架下进行讨论.在这方面,形式化语言XYZ/E可与其互补.XYZ/E是一种可执行线性时序逻辑语言,既可表示系统的性质,又可表示系统的行为.递归地在基本迁移系统上解释Statecharts语义,用XYZ/E公式表示它的时序语义.这一语义是模块级可组合的.求精过程的语义保持,可直接从语义定义得到保证.Statecharts所描述的系统行为模型和性质在同一个逻辑中表示,因此,系统行为是否满足所需性质的问题可由逻辑蕴涵式表示.

    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.

    参考文献
    [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
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:4773
  • 下载次数: 5877
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2004-07-29
  • 最后修改日期:2005-10-20
文章二维码
您是第19635944位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号