概率线性时段不变式的统计模型检验
2014-11-19 00:37安杰
电脑知识与技术 2014年30期
摘要：模型检验是软件工程形式化方法的一个重要组成部分，线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法，该方法针对不带有不确定性的概率模型，运用统计模型检验的方法，基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。
关键词：模型检验；时段验算；UPPAAL；概率线性时段不变式
中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2014）30-7097-03
随着计算机技术的飞速发展，计算机系统的规模和复杂性急剧增加，系统出错的概率随之增大。在一些重要的实时系统中，如航空交管、核电站监控等，任何错误都可能造成重大的经济损失和人员伤亡。如何在系统开发早期阶段验证设计的正确性，成为研究人员面对的重要问题。形式化方法（Formal Methods）是重要的提高系统可靠性和安全性的方法。模型检验（Model Checking）是形式化方法的重要组成部分。它是一种自动验证有穷状态系统的技术，通过穷举搜索状态空间来判断系统是否满足规约。时段验算（Duration Calculus）[1]是周巢尘院士提出的一种区间时态逻辑，用于描述系统的区间性质。线性时段不变式是时段验算性质的子集。
本文提出了对于一些概率系统，针对由概率线性时段不变式描述的系统性质的统计模型检验方法。该方法主要基于模型检验工具UPPAAL完成。主要思想是将概率线性时段不变式转化成概率计算树逻辑（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型检验。主要方法是在原自动机模型的基础上，引入辅助自动机，通过辅助自动机完成线性时段不变式的计算，由UPPAAL完成概率计算。
1 概率线性时段不变式
线性时段不变式（Linear duration invariants， LDI）是一类重要的时段演算公式，由周巢尘等人于1994年首次提出，实时系统中的许多安全性质都可以用这类公式进行描述。ProCos项目中的一个著名研究实例[29]就是对煤气燃烧器的需求进行形式化表述，比如对于需求——“如果对煤气燃烧器的观察时长l大于等于60秒，则燃气泄露时长不会超过整个观察时长的二十分之一”，就可以使用线性时段不变式来形式化地规约：
这里的leak是一个布尔函数，它表示煤气燃烧器是否处于漏气状态。注意，这里对该煤气燃烧器的观察是一个封闭区间。
然而，在实际情况下系统的行为往往是带有概率的。比如图1这样一个实际系统[3]。开始时，系统在状态s1，处于漏气状态，在该状态下它有两个选择，第一个选择是到达状态s2，第二个选择是到达状态s3，概率分别是0.2和0.8。在状态s2和s3 它们分别可以迁移到状态s3和s2，概率都是1。
对于这样的系统，线性时段不变式是否成立就会有一个概率值。
2 概率线性时段不变式的验证思路
给定由n个作为系统组件的时间自动机A1，A2，...，An构成的网络A=（L，s0，∑，X，I，E），以及线性时段不变式D，构造一个验证算法，来判断A是否满足D。[4]
只要限定D的前件中的a、b为整数（包含b为?的情形），则D就是可离散化性质。那么，只需检验A的所有整数行为对D的满足性，就可得知A的所有行为对D的满足性。所以，本节中规定，所有组件自动机都是整数时间自动机。
接着，简要描述验证过程的基本步骤：
1） 将每个组件自动机Ai改造成一个新的时间自动机gi。这种改造是为了标记系统A是否处于某个特定位置，能够帮助计算系统驻留该位置的时长；
2） 构造辅助验证的时间自动机S。在S中，引入两个变量gc和d，gc用于计算对于A的观察时长，d用于计算[（D）]的值；
3） 要求S与A并行执行，只要观察时长满足时限约束（即D的前件），则S会在观察中的每个整数时刻检验A对D的满足性。
4） 定义一个CTL公式
辅助自动机S如图2所示，其中，
· S有3个状态：初始状态，p0和p1。p0和p1上的约束均为x | 1；
· S有4条边：一条从初始状态连向p0的边，执行赋值语句x=1，使得验证最早能从0时刻开始；一条从p0连向p1的边，将变量gc和d初始化为0，用于在观察开始的瞬间检验D的真假；一条从p0连向自身的边，从A运行后一直保持空转，直至某时刻对A的观察正式开始才停止执行，而执行从p0至p1的边，使得观察能从A的任意可达状态开始；剩余一条从p1连向自身的边，它会执行验证函数accum（），用于实时更新gc和d的值；
· S有1个本地时钟：x，一旦其值累计至1就重置为0，表示只在整数时刻检验D的真假。
3 具体实验及分析
在试验中，我们针对图1中所描述的系统，在UPPAAL中景行具体实验。图3和图4分别是图1
中描述系统在UPPAAL中的模型以及统计模型检验得到的结果。
可以从结果中看出，对于图1中描述的系统，对于带概率的线性时段表达式的置信区间是[0.902606，1] 置信度为0.95。
4 结论
本文通过引入辅助自动机来完成对线性时段不变式的计算，基于UPPAAL完成了带概率的线性时段不变式的统计模型检验。
参考文献：
[1] 李晓山，周巢尘.时段演算综述[J].计算机学报， 1994， 17（11）： 842-851
[2] Baier C，Kwiatkowska M.Model Checking fora Probabilistic Branching Time Logic with Fairness[J].Distributed Computing，1998，11（3）：125—155.
[3] Dang Van Hung， MiaomiaoZhang.On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties[C].RTCSA，2007：165-172.
[4] Quan Zu， Miaomiao Zhang，Jiaqi Zhu.Bounded model-checking of discrete duration calculus[C].HSCC，2013：213-222.
摘要：模型检验是软件工程形式化方法的一个重要组成部分，线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法，该方法针对不带有不确定性的概率模型，运用统计模型检验的方法，基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。
关键词：模型检验；时段验算；UPPAAL；概率线性时段不变式
中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2014）30-7097-03
随着计算机技术的飞速发展，计算机系统的规模和复杂性急剧增加，系统出错的概率随之增大。在一些重要的实时系统中，如航空交管、核电站监控等，任何错误都可能造成重大的经济损失和人员伤亡。如何在系统开发早期阶段验证设计的正确性，成为研究人员面对的重要问题。形式化方法（Formal Methods）是重要的提高系统可靠性和安全性的方法。模型检验（Model Checking）是形式化方法的重要组成部分。它是一种自动验证有穷状态系统的技术，通过穷举搜索状态空间来判断系统是否满足规约。时段验算（Duration Calculus）[1]是周巢尘院士提出的一种区间时态逻辑，用于描述系统的区间性质。线性时段不变式是时段验算性质的子集。
本文提出了对于一些概率系统，针对由概率线性时段不变式描述的系统性质的统计模型检验方法。该方法主要基于模型检验工具UPPAAL完成。主要思想是将概率线性时段不变式转化成概率计算树逻辑（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型检验。主要方法是在原自动机模型的基础上，引入辅助自动机，通过辅助自动机完成线性时段不变式的计算，由UPPAAL完成概率计算。
1 概率线性时段不变式
线性时段不变式（Linear duration invariants， LDI）是一类重要的时段演算公式，由周巢尘等人于1994年首次提出，实时系统中的许多安全性质都可以用这类公式进行描述。ProCos项目中的一个著名研究实例[29]就是对煤气燃烧器的需求进行形式化表述，比如对于需求——“如果对煤气燃烧器的观察时长l大于等于60秒，则燃气泄露时长不会超过整个观察时长的二十分之一”，就可以使用线性时段不变式来形式化地规约：
这里的leak是一个布尔函数，它表示煤气燃烧器是否处于漏气状态。注意，这里对该煤气燃烧器的观察是一个封闭区间。
然而，在实际情况下系统的行为往往是带有概率的。比如图1这样一个实际系统[3]。开始时，系统在状态s1，处于漏气状态，在该状态下它有两个选择，第一个选择是到达状态s2，第二个选择是到达状态s3，概率分别是0.2和0.8。在状态s2和s3 它们分别可以迁移到状态s3和s2，概率都是1。
对于这样的系统，线性时段不变式是否成立就会有一个概率值。
2 概率线性时段不变式的验证思路
给定由n个作为系统组件的时间自动机A1，A2，...，An构成的网络A=（L，s0，∑，X，I，E），以及线性时段不变式D，构造一个验证算法，来判断A是否满足D。[4]
只要限定D的前件中的a、b为整数（包含b为?的情形），则D就是可离散化性质。那么，只需检验A的所有整数行为对D的满足性，就可得知A的所有行为对D的满足性。所以，本节中规定，所有组件自动机都是整数时间自动机。
接着，简要描述验证过程的基本步骤：
1） 将每个组件自动机Ai改造成一个新的时间自动机gi。这种改造是为了标记系统A是否处于某个特定位置，能够帮助计算系统驻留该位置的时长；
2） 构造辅助验证的时间自动机S。在S中，引入两个变量gc和d，gc用于计算对于A的观察时长，d用于计算[（D）]的值；
3） 要求S与A并行执行，只要观察时长满足时限约束（即D的前件），则S会在观察中的每个整数时刻检验A对D的满足性。
4） 定义一个CTL公式
辅助自动机S如图2所示，其中，
· S有3个状态：初始状态，p0和p1。p0和p1上的约束均为x | 1；
· S有4条边：一条从初始状态连向p0的边，执行赋值语句x=1，使得验证最早能从0时刻开始；一条从p0连向p1的边，将变量gc和d初始化为0，用于在观察开始的瞬间检验D的真假；一条从p0连向自身的边，从A运行后一直保持空转，直至某时刻对A的观察正式开始才停止执行，而执行从p0至p1的边，使得观察能从A的任意可达状态开始；剩余一条从p1连向自身的边，它会执行验证函数accum（），用于实时更新gc和d的值；
· S有1个本地时钟：x，一旦其值累计至1就重置为0，表示只在整数时刻检验D的真假。
3 具体实验及分析
在试验中，我们针对图1中所描述的系统，在UPPAAL中景行具体实验。图3和图4分别是图1
中描述系统在UPPAAL中的模型以及统计模型检验得到的结果。
可以从结果中看出，对于图1中描述的系统，对于带概率的线性时段表达式的置信区间是[0.902606，1] 置信度为0.95。
4 结论
本文通过引入辅助自动机来完成对线性时段不变式的计算，基于UPPAAL完成了带概率的线性时段不变式的统计模型检验。
参考文献：
[1] 李晓山，周巢尘.时段演算综述[J].计算机学报， 1994， 17（11）： 842-851
[2] Baier C，Kwiatkowska M.Model Checking fora Probabilistic Branching Time Logic with Fairness[J].Distributed Computing，1998，11（3）：125—155.
[3] Dang Van Hung， MiaomiaoZhang.On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties[C].RTCSA，2007：165-172.
[4] Quan Zu， Miaomiao Zhang，Jiaqi Zhu.Bounded model-checking of discrete duration calculus[C].HSCC，2013：213-222.
摘要：模型检验是软件工程形式化方法的一个重要组成部分，线性时段不变式是形式化方法中表述系统性质的一种重要表达式。对线性时段不变式的模型检验一直是形式化方法研究的一个重要内容。该文提出了一种针对带概率的线性时段不变式的模型检验方法，该方法针对不带有不确定性的概率模型，运用统计模型检验的方法，基于UPPAAL工具实现了概率线性时段不变式的统计模型检验。
关键词：模型检验；时段验算；UPPAAL；概率线性时段不变式
中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2014）30-7097-03
随着计算机技术的飞速发展，计算机系统的规模和复杂性急剧增加，系统出错的概率随之增大。在一些重要的实时系统中，如航空交管、核电站监控等，任何错误都可能造成重大的经济损失和人员伤亡。如何在系统开发早期阶段验证设计的正确性，成为研究人员面对的重要问题。形式化方法（Formal Methods）是重要的提高系统可靠性和安全性的方法。模型检验（Model Checking）是形式化方法的重要组成部分。它是一种自动验证有穷状态系统的技术，通过穷举搜索状态空间来判断系统是否满足规约。时段验算（Duration Calculus）[1]是周巢尘院士提出的一种区间时态逻辑，用于描述系统的区间性质。线性时段不变式是时段验算性质的子集。
本文提出了对于一些概率系统，针对由概率线性时段不变式描述的系统性质的统计模型检验方法。该方法主要基于模型检验工具UPPAAL完成。主要思想是将概率线性时段不变式转化成概率计算树逻辑（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型检验。主要方法是在原自动机模型的基础上，引入辅助自动机，通过辅助自动机完成线性时段不变式的计算，由UPPAAL完成概率计算。
1 概率线性时段不变式
线性时段不变式（Linear duration invariants， LDI）是一类重要的时段演算公式，由周巢尘等人于1994年首次提出，实时系统中的许多安全性质都可以用这类公式进行描述。ProCos项目中的一个著名研究实例[29]就是对煤气燃烧器的需求进行形式化表述，比如对于需求——“如果对煤气燃烧器的观察时长l大于等于60秒，则燃气泄露时长不会超过整个观察时长的二十分之一”，就可以使用线性时段不变式来形式化地规约：
这里的leak是一个布尔函数，它表示煤气燃烧器是否处于漏气状态。注意，这里对该煤气燃烧器的观察是一个封闭区间。
然而，在实际情况下系统的行为往往是带有概率的。比如图1这样一个实际系统[3]。开始时，系统在状态s1，处于漏气状态，在该状态下它有两个选择，第一个选择是到达状态s2，第二个选择是到达状态s3，概率分别是0.2和0.8。在状态s2和s3 它们分别可以迁移到状态s3和s2，概率都是1。
对于这样的系统，线性时段不变式是否成立就会有一个概率值。
2 概率线性时段不变式的验证思路
给定由n个作为系统组件的时间自动机A1，A2，...，An构成的网络A=（L，s0，∑，X，I，E），以及线性时段不变式D，构造一个验证算法，来判断A是否满足D。[4]
只要限定D的前件中的a、b为整数（包含b为?的情形），则D就是可离散化性质。那么，只需检验A的所有整数行为对D的满足性，就可得知A的所有行为对D的满足性。所以，本节中规定，所有组件自动机都是整数时间自动机。
接着，简要描述验证过程的基本步骤：
1） 将每个组件自动机Ai改造成一个新的时间自动机gi。这种改造是为了标记系统A是否处于某个特定位置，能够帮助计算系统驻留该位置的时长；
2） 构造辅助验证的时间自动机S。在S中，引入两个变量gc和d，gc用于计算对于A的观察时长，d用于计算[（D）]的值；
3） 要求S与A并行执行，只要观察时长满足时限约束（即D的前件），则S会在观察中的每个整数时刻检验A对D的满足性。
4） 定义一个CTL公式
辅助自动机S如图2所示，其中，
· S有3个状态：初始状态，p0和p1。p0和p1上的约束均为x | 1；
· S有4条边：一条从初始状态连向p0的边，执行赋值语句x=1，使得验证最早能从0时刻开始；一条从p0连向p1的边，将变量gc和d初始化为0，用于在观察开始的瞬间检验D的真假；一条从p0连向自身的边，从A运行后一直保持空转，直至某时刻对A的观察正式开始才停止执行，而执行从p0至p1的边，使得观察能从A的任意可达状态开始；剩余一条从p1连向自身的边，它会执行验证函数accum（），用于实时更新gc和d的值；
· S有1个本地时钟：x，一旦其值累计至1就重置为0，表示只在整数时刻检验D的真假。
3 具体实验及分析
在试验中，我们针对图1中所描述的系统，在UPPAAL中景行具体实验。图3和图4分别是图1
中描述系统在UPPAAL中的模型以及统计模型检验得到的结果。
可以从结果中看出，对于图1中描述的系统，对于带概率的线性时段表达式的置信区间是[0.902606，1] 置信度为0.95。
4 结论
本文通过引入辅助自动机来完成对线性时段不变式的计算，基于UPPAAL完成了带概率的线性时段不变式的统计模型检验。
参考文献：
[1] 李晓山，周巢尘.时段演算综述[J].计算机学报， 1994， 17（11）： 842-851
[2] Baier C，Kwiatkowska M.Model Checking fora Probabilistic Branching Time Logic with Fairness[J].Distributed Computing，1998，11（3）：125—155.
[3] Dang Van Hung， MiaomiaoZhang.On Verification of Probabilistic Timed Automata against Probabilistic Duration Properties[C].RTCSA，2007：165-172.
[4] Quan Zu， Miaomiao Zhang，Jiaqi Zhu.Bounded model-checking of discrete duration calculus[C].HSCC，2013：213-222.
