连续时段演算的模型检验

发布时间：2018-05-29 03:01

本文选题：模型检验 + 时间自动机　；参考：《电脑知识与技术》2016年28期

【摘要】：模型检验是一种对有限状态系统的性质进行自动检验的技术,能够对系统设计的正确性进行验证。线性时段不变式是一类重要的时段演算公式,它用来描述实时系统的安全性质。而扩展线性时段不变式通过命题逻辑和"切变"运算对线性时段不变式进行了扩展,是更有表达力的时段演算公式。由于扩展线性时段不变式不能通过其离散语义下的满足性来等价于其连续语义下的满足性,离散时间下的模型检验算法并不适用于连续时间的情况,因此研究连续时间下扩展线性时段不变式的模型检验方法对于实时系统的性质检验具有重要的实用意义。该文提出了连续时间下针对扩展线性时段不变式的有界模型检验算法,根据离散化方法将连续时间下的问题转化为离散情况,通过迭代地调用离散时间下线性时段不变式的有界模型检验算法,来解决研究的问题。实验表明,该文提出的算法能够有效地对连续时间下的扩展线性时段不变式进行有界模型检验。
[Abstract]:Model checking is a kind of automatic verification technology for the properties of finite state system, which can verify the correctness of system design. Linear time invariant is a kind of important time interval calculus formula, which is used to describe the security property of real time system. The extended linear time invariant extends the linear period invariant by propositional logic and "shear" operation, which is a more expressive formula of time interval calculus. Because the extended linear time invariant can not be equivalent to the satisfaction under its continuous semantics by the satisfaction of its discrete semantics, the model checking algorithm in discrete time is not suitable for continuous time. Therefore, it is of great practical significance to study the model checking method of extended linear time invariant in continuous time for the property test of real time systems. In this paper, a bounded model checking algorithm for the invariant of extended linear time period in continuous time is proposed. According to the discretization method, the problem under continuous time is transformed into discrete case. The problem is solved by iteratively calling the bounded model checking algorithm of linear time invariant in discrete time. Experiments show that the proposed algorithm can effectively test the extended linear time invariant in continuous time.
【作者单位】：同济大学;
【基金】：扩展的线性时段不变式的模型检验(项目编号:F020106)
【分类号】：TP311.53

【相似文献】