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

摘要

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