消息顺序图规范的时间一致性检验工具

摘要：

对于实时系统,消息顺序图(Message Sequence Chart,以下简称MSC)描述了系统中各部件间的交互活动.消息顺序图规范(MSC Specifications,以下简称MSS)能方便地表示多个场景并提供了一种直观可视的方法来描述设计需求.但是,如同其它的规范和设计过程,MSC也很容易出错,所以对它们进行分析是很有必要的.本文分析了带时间约束的MSS,并给出了一个检验MSS时间一致性的工具的设计和实现过程.

关键词： 实时系统 消息顺序图规范 模型检验 时间一致性

作者: 谭文凯 南京大学计算机科学与技术系(南京) 李宣东 南京大学计算机科学与技术系(南京) 郑国梁 南京大学计算机科学与技术系(南京)

作者单位: 南京大学计算机软件新技术国家重点实验室(南京)

会议类型: 国内会议

会议名称: 863计划智能计算机主题学术会议

会议地点: 北京

会议语种:中文

页码: 515-522

在线出版日期: 2001-02-01（万方平台首次上网日期，不代表论文的发表时间）