模态顺序图uMSD的形式语义

• 作者: 张鹏程 李雯睿 王志坚
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模态顺序图 弱交换Büchi自动机 性质规约模式
• 年，卷（期）: 2011,（4）
• 所属期刊栏目: 系统软件与软件工程
• 页码范围: 659-675
• 分类号: TP311
• 字数: 9783字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.03776

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王志坚	河海大学计算机及信息工程学院	212	2079	22.0	37.0
2	李雯睿	河海大学计算机及信息工程学院	4	25	3.0	4.0
11	张鹏程	河海大学计算机及信息工程学院	35	115	8.0	8.0