一类并发实时系统的自动验证

• 作者: Dan Van Hung 赵建华 郑国梁
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型验证 实时系统
• 年，卷（期）: 2000,（2）
• 页码范围: 229-234
• 页数: 6页
• 分类号: TP311
• 字数: 5214字
• 语种: 中文

摘要

一个被广泛用于验证实时系统的方法是根据被验证的实时性质,使用适当的双向模拟等价关系使无限的状态空间转化为有限的状态等价类空间.算法只需要在这个有限的等价类空间里搜索就可以得到正确答案.但是,这个等价类空间的规模一般随着系统规模的增大而产生爆炸性的增长,以至于在很多情况下,穷尽搜索这个空间是不现实的.该文引入了一个等价关系来验证一个由多个实时自动机通过共享变量组成的并发系统是否满足一个线性时段特性.同时,还引入了格局之间的兼容关系来避免对状态等价类空间的穷尽搜索.基于这两个关系,文章提出了一个算法来验证是否一个实时自动机网满足一个线性时段特性.实例研究显示,此算法在某些情况下比其他一些工具有更好的时间和空间效率.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郑国梁	南京大学计算机科学与技术系	77	1523	21.0	37.0
2	赵建华	南京大学计算机科学与技术系	23	201	7.0	13.0
3	Dan Van Hung	联合国大学国际软件研究所	1	3	1.0	1.0