|
|||||
|
|
| 模态顺序图uMSD 的形式语义 | |
| 引用本文： | 李雯睿,王志坚,张鹏程. 模态顺序图uMSD 的形式语义[J]. 软件学报, 2011, 22(4): 659-675. DOI: 10.3724/SP.J.1001.2011.03776 |
| 作者姓名： | 李雯睿 王志坚 张鹏程 |
| 作者单位： | 1. 河海大学,计算机及信息工程学院,江苏,南京,210098;南京晓庄学院,数学与信息技术学院,江苏,南京,211171;武汉大学,软件工程国家重点实验室,湖北,武汉,430072 2. 河海大学,计算机及信息工程学院,江苏,南京,210098 3. 河海大学,计算机及信息工程学院,江苏,南京,210098;武汉大学,软件工程国家重点实验室,湖北,武汉,430072 |
| 基金项目： | 国家高技术研究发展计划(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的表达能力.最后进行了实例研究,并讨论了其应用前景. |
| 关 键 词： | 模态顺序图 弱交换Büchi自动机 性质规约模式 |
| 收稿时间： | 2009-03-25 |
| 修稿时间： | 2009-10-23 |
Formal Semantics of Universal Modal Sequence Diagram |
|
| LI Wen-Rui,WANG Zhi-Jian and ZHANG Peng-Cheng. Formal Semantics of Universal Modal Sequence Diagram[J]. Journal of Software, 2011, 22(4): 659-675. DOI: 10.3724/SP.J.1001.2011.03776 | |
| Authors: | LI Wen-Rui WANG Zhi-Jian ZHANG Peng-Cheng |
| Affiliation: | College of Computer and Information Engineering, Hohai University, Nanjing 210098, China;School of Mathematics and Information Technology, Nanjing Xiaozhuang University, Nanjing 211171, China;State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China;College of Computer and Information Engineering, Hohai University, Nanjing 210098, China;College of Computer and Information Engineering, Hohai University, Nanjing 210098, China;State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, China |
| Abstract: | 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. |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《软件学报》浏览原始摘要信息 | |
| 点击此处可从《软件学报》下载全文 | |