模态顺序图uMSD 的形式语义
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

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


Formal Semantics of Universal Modal Sequence Diagram
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    UML 2.0 顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0 顺序图的模态扩展,区分了强制场景(用universal MSD 表示,简称uMSD)和可能场景(用existential MSD 表示,简称eMSD).其中,uMSD 具有较强的表达能力,能够用于表示并发系统的时态性质,故主要工作围绕uMSD 展开.为了使uMSD 用于形式化分析、验证和监控,给出基于自动机的uMSD 语义解释,并给出各种操作符的算法,用性质规约模式度量uMSD 的表达能力.最后进行了实例研究,并讨论了其应用前景.

    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.

    参考文献
    相似文献
    引证文献
引用本文

李雯睿,王志坚,张鹏程.模态顺序图uMSD 的形式语义.软件学报,2011,22(4):659-675

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

京公网安备 11040202500063号