论文部分内容阅读
近些年来,基于SMT的限界模型检测方法作为基于SAT的限界模型检测方法的一种改进,在对实时系统的检测上已经得到了一定发展.一直以来,限界模型检测多被用于检验存在性性质,而很少用于验证全局性性质,原因之一就是该方法受界限的限制,很难实现对全局性性质的有效编码.为此,通过对传统限界模型检测中的编码方式进行相应改变,在一定程度上解决了这一问题.同时,结合SMT,实现了对实时系统中某些全局性性质的验证.实验表明该方法比已有的方法效率更高.