论文部分内容阅读
基于SAT的限界模型检测在处理实时系统时具有很高的复杂度．SMT求解器在计算可满足性的同时，还能处理算术和其他可判定性理论．在对实时系统进行检测时，用SMT求解器代替SAT求解器，系统里的时钟就可以用整型或实型变量表示，时钟约束则可以直接表示成线性算术表达式，从而使整个检测过程更加高效．带时间参数的计算树逻辑（timed computation tree logic，简称TCTL）被用来描述实时系统里的性质．同时，还对检测方法作了相应的改进．