一种层次式时间自动机模型检测方法 |
| |
引用本文: | 周宇,胡军,葛季栋.一种层次式时间自动机模型检测方法[J].计算机应用与软件,2012(11). |
| |
作者姓名: | 周宇 胡军 葛季栋 |
| |
作者单位: | 1. 南京航空航天大学计算机科学与技术学院 江苏 南京210000 2. 南京大学软件新技术国家重点实验室 江苏 南京210000 |
| |
摘 要: | 层次式时间自动机在软件系统建模过程中有着重要的应用.由于层次嵌套带来额外的复杂度,难以对之进行直接的形式化验证工作.提出一种平展算法,将层次式时间自动机转化为一组并行的顺序时间自动机,应用广播通道同步该自动机集合执行.在此基础之上实现一个原型系统可以将层次式时间自动机模型自动转化为模型检测工具UPPAAL的输入,从而可以对之进行验证.结合实时UML状态机图实例,证明了该方法的有效性.
|
关 键 词: | 层次式时间自动机 形式化方法 模型检测 |
本文献已被 万方数据 等数据库收录! |
|