论文部分内容阅读
摘要：模型检验是一种对有限状态系统的性质进行自动检验的技术，能够对系统设计的正确性进行验证。线性时段不变式是一类重要的时段演算公式，它用来描述实时系统的安全性质。而扩展线性时段不变式通过命题逻辑和“切变”运算对线性时段不变式进行了扩展，是更有表达力的时段演算公式。由于扩展线性时段不变式不能通过其离散语义下的满足性来等价于其连续语义下的满足性，离散时间下的模型检验算法并不适用于连续时间的情况，因此研究连续时间下扩展线性时段不变式的模型检验方法对于实时系统的性质检验具有重要的实用意义。该文提出了连续时间下针对扩展线性时段不变式的有界模型检验算法，根据离散化方法将连续时间下的问题转化为离散情况，通过迭代地调用离散时间下线性时段不变式的有界模型检验算法，来解决研究的问题。实验表明，该文提出的算法能够有效地对连续时间下的扩展线性时段不变式进行有界模型检验。
关键词：模型检验；时间自动机；连续时段演算；切变
中图分类号：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性质的条件是的所有迁移路径满足，即。对于任意不满足性质的自动机，能且至少能够找到一条不满足待检验性质。
3时段演算的模型检验
对于时间自动机，其模型检验的步骤如下：
1） 找出时间自动机在检验时间区间[]的所有运行路径；
2） 对于形如，其中，计，确定检验范围内潜在的切变点；
3） 对于任意一条迁移路径，计算潜在切变点下的可能取值组合，满足所有的切变点即为有效切变点；
4） 讨论有效切变点下内所有迁移路径，若所有路径都满足性质，则表明该自动机能够找到满足性质的切变点，即自动机满足性质。
现给出待检验的自动机及ELDI性质，具体说明检验过程：
ELDI性质：
该性质表示，从任意时刻为初始时刻对系统进行观测，当观测时长为2时，要求寻找到一时间点，使得时段内系统满足，其中。以初始观测时刻为0为例，在观测时长为2的情况下，能够找到的离散切变点可能有3个，0，1和2，而可能的连续切变点则为无数个。
因此可以得出结论，在离散语义下，该自动机不满足性质，即。 然而对于实际运行状态下的系统，时间并非简单的离散值，更有可能是连续值，因此对于离散语义下的模型检验结果并不能完全代表系统的检验结果，对于连续语义下的模型检验更有必要。
在连续语义下，自动机的时钟变量和迁移时刻均有可能是连续值，而切变点也可能是连续值，因此首先定性地分析离散之间自动机对连续ELDI性质的模型检验，即是否能够找到连续的切变点，使得所有离散的迁移路径能够满足性质。
由于模型检验工具仅支持时间约束和时间变量为整数的检验，通过离散化和微积分的思想可以用有限的若干离散值表示无限的连续值的情况，具体可以改变时间自动机中的时间约束和ELDI的系数，改造出若干连续点。
以上述检验过程为例，通过将时间自动机的所有时间约束扩大3倍，同时ELDI中的观测时长也变为3倍，即可得到单位为原自动机1/3长度的迁移路径，如一条路径：，其时间约束都乘以3倍后得到的迁移路径长度为6，对应的该路径可能变为：。由于此时该路径的时长为6，对于该自动机则产生了新的路径，如，不难理解该条路径等价于原来的。同时由于观测时长也扩大了3倍，在给定的观测时长为6的情况下，则产生了多个连续的切变点。通过这种方式可以讨论一些连续迁移路径和连续切变点的情况。
根据计算，在此情况下，起始时刻3个时间单位后的点为切变点，此时所有路径均满足该切变点，即存在实际切变点1.5，使得该自动机满足ELDI性质
因此，在该计算方法下，能够找到使得系统满足的连续切变点，即实验证明：。
4实验分析与结论
在实验中，我们发现该方法能够解决一部分连续时段演算的模型检验要求，对单切变点和多切变点情况均适用，并得出较离散语义下更为准确的检验结果，为一部分离散模型检验下不满足的系统找到能够满足性质的连续切变点。然而对于另一部分仍无法找到连续切变点的时间自动机，需要进行严格的语义规约及定性检验，仅对一部分单切变点的模型检验找到连续迁移路径下的离散规约方法，并进行检验。
从实际工程应用的角度来说，连续时段演算下的模型检验在工程上具有重要的意义。它保证了实际应用中相关具有连续性的机械设备、通信协议等系统在时间规约性质上的准确性和可靠性，对验证具有连续时间意义的性质的系统验证研究具有实际意义。
参考文献：
[1] Edmund M Clarke， Orna Grumberg， Doron A Peled. Model Checking[M]. The MIT Press， 1999.
[2] Chaochen Zhou. Linear duration invariants[C]. In FTRTFT 1994， 1994： 86–109.
[3] Zu Q， Zhang M， Zhu J， et al. Bounded model-checking of discrete duration calculus[C]//Proceedings of the 16th international conference on Hybrid systems： computation and control. ACM， 2013： 213-222.
[4] 李晓山， 周巢尘.时段演算综述[J].计算机学报， 1994，17（11）： 842-851.
[5] Rajeev Alur ，David L Dill. A theory of timed automata[C]. Theoretical Computer Science， 126（2）：183–235， 1994.
关键词：模型检验；时间自动机；连续时段演算；切变
中图分类号：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性质的条件是的所有迁移路径满足，即。对于任意不满足性质的自动机，能且至少能够找到一条不满足待检验性质。
3时段演算的模型检验
对于时间自动机，其模型检验的步骤如下：
1） 找出时间自动机在检验时间区间[]的所有运行路径；
2） 对于形如，其中，计，确定检验范围内潜在的切变点；
3） 对于任意一条迁移路径，计算潜在切变点下的可能取值组合，满足所有的切变点即为有效切变点；
4） 讨论有效切变点下内所有迁移路径，若所有路径都满足性质，则表明该自动机能够找到满足性质的切变点，即自动机满足性质。
现给出待检验的自动机及ELDI性质，具体说明检验过程：
ELDI性质：
该性质表示，从任意时刻为初始时刻对系统进行观测，当观测时长为2时，要求寻找到一时间点，使得时段内系统满足，其中。以初始观测时刻为0为例，在观测时长为2的情况下，能够找到的离散切变点可能有3个，0，1和2，而可能的连续切变点则为无数个。
因此可以得出结论，在离散语义下，该自动机不满足性质，即。 然而对于实际运行状态下的系统，时间并非简单的离散值，更有可能是连续值，因此对于离散语义下的模型检验结果并不能完全代表系统的检验结果，对于连续语义下的模型检验更有必要。
在连续语义下，自动机的时钟变量和迁移时刻均有可能是连续值，而切变点也可能是连续值，因此首先定性地分析离散之间自动机对连续ELDI性质的模型检验，即是否能够找到连续的切变点，使得所有离散的迁移路径能够满足性质。
由于模型检验工具仅支持时间约束和时间变量为整数的检验，通过离散化和微积分的思想可以用有限的若干离散值表示无限的连续值的情况，具体可以改变时间自动机中的时间约束和ELDI的系数，改造出若干连续点。
以上述检验过程为例，通过将时间自动机的所有时间约束扩大3倍，同时ELDI中的观测时长也变为3倍，即可得到单位为原自动机1/3长度的迁移路径，如一条路径：，其时间约束都乘以3倍后得到的迁移路径长度为6，对应的该路径可能变为：。由于此时该路径的时长为6，对于该自动机则产生了新的路径，如，不难理解该条路径等价于原来的。同时由于观测时长也扩大了3倍，在给定的观测时长为6的情况下，则产生了多个连续的切变点。通过这种方式可以讨论一些连续迁移路径和连续切变点的情况。
根据计算，在此情况下，起始时刻3个时间单位后的点为切变点，此时所有路径均满足该切变点，即存在实际切变点1.5，使得该自动机满足ELDI性质
因此，在该计算方法下，能够找到使得系统满足的连续切变点，即实验证明：。
4实验分析与结论
在实验中，我们发现该方法能够解决一部分连续时段演算的模型检验要求，对单切变点和多切变点情况均适用，并得出较离散语义下更为准确的检验结果，为一部分离散模型检验下不满足的系统找到能够满足性质的连续切变点。然而对于另一部分仍无法找到连续切变点的时间自动机，需要进行严格的语义规约及定性检验，仅对一部分单切变点的模型检验找到连续迁移路径下的离散规约方法，并进行检验。
从实际工程应用的角度来说，连续时段演算下的模型检验在工程上具有重要的意义。它保证了实际应用中相关具有连续性的机械设备、通信协议等系统在时间规约性质上的准确性和可靠性，对验证具有连续时间意义的性质的系统验证研究具有实际意义。
参考文献：
[1] Edmund M Clarke， Orna Grumberg， Doron A Peled. Model Checking[M]. The MIT Press， 1999.
[2] Chaochen Zhou. Linear duration invariants[C]. In FTRTFT 1994， 1994： 86–109.
[3] Zu Q， Zhang M， Zhu J， et al. Bounded model-checking of discrete duration calculus[C]//Proceedings of the 16th international conference on Hybrid systems： computation and control. ACM， 2013： 213-222.
[4] 李晓山， 周巢尘.时段演算综述[J].计算机学报， 1994，17（11）： 842-851.
[5] Rajeev Alur ，David L Dill. A theory of timed automata[C]. Theoretical Computer Science， 126（2）：183–235， 1994.