模态顺序图uMSD的形式语义  

Formal Semantics of Universal Modal Sequence Diagram

作　　者：李雯睿[1,2,1] 王志坚[1] 张鹏程[1,1] 

机构地区：[1]河海大学计算机及信息工程学院,江苏南京210098 [2]南京晓庄学院数学与信息技术学院,江苏南京211171

出　　处：《软件学报》2011年第4期659-675,共17页Journal of Software

基　　金：国家高技术研究发展计划(863)(2007AA01Z178);中央高校基本科研业务费专项资金(2009B04314);武汉大学软件工程国家重点实验室开放基金(2010-08-01)

摘　　要：UML 2.0顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0顺序图的模态扩展,区分了强制场景(用universal MSD表示,简称uMSD)和可能场景(用existential MSD表示,简称eMSD).其中,uMSD具有较强的表达能力,能够用于表示并发系统的时态性质,故主要工作围绕uMSD展开.为了使uMSD用于形式化分析、验证和监控,给出基于自动机的uMSD语义解释,并给出各种操作符的算法,用性质规约模式度量uMSD的表达能力.最后进行了实例研究,并讨论了其应用前景.The UML 2.0 Sequence Diagram has been extensively applied in industry.However,the vague semantics of UML 2.0 Sequence Diagram prevent it from being applied effectively.Modal Sequence Diagram is the modal extension of UML 2.0 Sequence Diagram,which distinguishes mandatory scenarios（described by universal MSD,denoted as uMSD） from possible scenarios（described by existential MSD,denoted as eMSD）.uMSD is more expressive than eMSD and can represent the temporal properties of concurrent systems.Therefore,the main work of the paper is on uMSD.In order to make uMSD extensively used for formal analysis,verification,and monitoring,the formal semantics of uMSD,based on the Weak Alternating Büchi automaton,are represented,and the transformation algorithms of various operators are given in detail.Next,the expressiveness of uMSD is measured by the well known property specification patterns.Finally,an example is studied,and its future applications are discussed.

关 键 词：模态顺序图 弱交换Büchi自动机 性质规约模式 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]