一种层次式时间自动机模型检测方法

• 作者: 周宇 胡军 葛季栋
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 层次式时间自动机 形式化方法 模型检测
• 年，卷（期）: 2012,（11）
• 页码范围: 48-51
• 分类号: TP301
• 字数: 4339字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2012.11.013

摘要

层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周宇	南京航空航天大学计算机科学与技术学院	18	70	4.0	8.0
2	葛季栋	南京大学软件新技术国家重点实验室	12	88	5.0	9.0
3	胡军	南京航空航天大学计算机科学与技术学院	41	358	10.0	18.0