连续时段演算的模型检验

模型检验是一种对有限状态系统的性质进行自动检验的技术,能够对系统设计的正确性进行验证.线性时段不变式是一类重要的时段演算公式,它用来描述实时系统的安全性质.而扩展线性时段不变式通过命题逻辑和＆quot;切变＆quot;运算对线性时段不变式进行了扩展,是更有表达力的时段演算公式.由于扩展线性时段不变式不能通过其离散语义下的满足性来等价于其连续语义下的满足性,离散时间下的模型检验算法并不适用于连续时间的情况,因此研究连续时间下扩展线性时段不变式的模型检验方法对于实时系统的性质检验具有重要的实用意义.该文提出了连续时间下针对扩展线性时段不变式的有界模型检验算法,根据离散化方法将连续时间下的问题转化为离散情况,通过迭代地调用离散时间下线性时段不变式的有界模型检验算法,来解决研究的问题.实验表明,该文提出的算法能够有效地对连续时间下的扩展线性时段不变式进行有界模型检验.