连续时段演算的模型检验.docVIP

连续时段演算的模型检验 　　摘要：模型检验是一种对有限状态系统的性质进行自动检验的技术，能够对系统设计的正确性进行验证。线性时段不变式是一类重要的时段演算公式，它用来描述实时系统的安全性质。而扩展线性时段不变式通过命题逻辑和“切变”运算对线性时段不变式进行了扩展，是更有表达力的时段演算公式。由于扩展线性时段不变式不能通过其离散语义下的满足性来等价于其连续语义下的满足性，离散时间下的模型检验算法并不适用于连续时间的情况，因此研究连续时间下扩展线性时段不变式的模型检验方法对于实时系统的性质检验具有重要的实用意义。该文提出了连续时间下针对扩展线性时段不变式的有界模型检验算法，根据离散化方法将连续时间下的问题转化为离散情况，通过迭代地调用离散时间下线性时段不变式的有界模型检验算法，来解决研究的问题。实验表明，该文提出的算法能够有效地对连续时间下的扩展线性时段不变式进行有界模型检验。 　　关键词：模型检验；时间自动机；连续时段演算；切变 　　中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2016）28-0109-03 　　1绪论 　　随着计算机技术的飞速发展，软件系统日趋复杂，计算机系统的规模和复杂性与日俱增，系统潜在的任何问题都可能引发严重的后果。因此，如何在系统开发早期阶段验证设计的正确性和可靠性，成为软件工程领域研究的重点课题。形式化方法（FormalMethod）是一种用于提高系统可靠性和安全性的重要方法。模型检验（Model Checking）[1]是形式化方法的重要组成部分，它是一种自动验证有穷状态系统的技术。时段演算（Duration Calculus）[2]是一种区间时态逻辑，用于表示系统在区间上的性质。线性时段不变式和扩展线性时段不变式都是重要的时段演算表达式。 　　本文提出了一种针对连续时态语义下由扩展线性时段不变式描述的系统性质的模型检验方法。该方法主要基于模型检验工具UPPAAL完成。主要思想是将连续语义下的时段演算的模型检验转化为离散语义下的模型检验，基于离散语义下的时段演算方法[3]，对其进行转化和改造，形成连续时段演算的模型检验方法。 　　2 基础理论 　　2.1 时段演算 　　时段演算是一种区间时序逻辑，它将布尔函数在区间上的积分进行形式化，用来表述和推理实时系统的定量性质。线性时段不变式是一类重要的时段演算公式，实时系统中的许多安全性质都可以用线性时段不变式进行规约。而扩展的线性时段不变式是对于线性时段不变式的扩展，它是更具有表达力的时段演算公式，因此本文主要以扩展线性时段不变式为研究对象进行论述。 　　2.2扩展线性时段不变式 　　扩展线性时段不变式（Extended Linear Duration Invariants，ELDI）[4]是对普通线性时段不变式在切变（chop，符号；）语义上扩展形成的，形如ELDI，它表示从初始时间0时刻开始，对系统进行观测，当观测时长在[]区间内时，要求系统处于某个状态的累积时间长度满足，其中、、、为实数，为系统状态，则该系统满足性质。ProCos项目中的一个著名研究实例就是对煤气燃烧器的需求进行形式化表述，比如对于需求：“如果对煤气燃烧器的观察时长大于等于60秒，则燃气泄露时长不会超过整个观察时长的二十分之一”，即可使用ELDI来形式化地规约：这里的是一个布尔函数，它表示煤气燃烧器是否处于漏气状态。注意，这里对该煤气燃烧器的观察是一个封闭区间。 　　此外，还有一种经过chop（）语义扩展的ELDI，形如，其中。对于chop语义的理解如下，。即在观测时段范围内，存在一个点m使得性质在的时段内成立，而性质在的时段内成立，如图1所示。 　　2.3 时间自动机 　　时间自动机（Timed Automata）[5]理论是实时系统最常用的表示模型，它所建立的模型用于描述时间系统的行为，它作为有限时间自动机的时间扩展，在其基础上增加了时间变量和约束条件。时间自动机使用有限数量的变量来表示时间，称为时间变量；同时用一个约束条件来注释状态转换图，用于决定状态转换发生的时间限制，也称为时间约束。对于具有时间行为的系统，如实时系统等，时间自动机可被用来对其行为进行建模和分析，进一步检验系统的性质。 　　在对时间自动机进行性质规约的模型检验时，有时会引入离散时间语义作为背景，表示验证过程只考虑该时间自动机的整数行为，简称为离散时间自动机；相反，连续时间语义下的验证过程中，我们简称时间自动机为连续时间自动机。 　　时间自动机从一个状态到另一个状态的转换称为迁移。模型检验通过时间自动机的迁移路径对验证性质的满足性进行判定，对于时间自动机，满足ELDI性质的条件是的所有迁移路径满足，即。对于任意不满足性质的自动机，能且至少能够找到