概率时段演算的模型检验概述

2015-01-06吴敏

电脑知识与技术 2014年34期

吴敏

摘要：在实际工程应用中，越来越多的系统表现出具有概率性等特征。作为对于此类实时系统的建模，概率时间自动机因为其能同时表示概率性、随机性和不确定性而被广泛采用。在对此类带概率性质的实时系统进行描述时，作为时段演算的一种扩展，概率时段演算被用来计算此类系统满足需求的概率。该文主要概述基于概率时间自动机的概率时段演算的模型检验主要步骤及其核心算法，其中模型检验的核心算法通过分别将前两者转换为区域图和概率分支时间逻辑来达成。

关键词：实时系统；模型检验；概率时间自动机；概率时段演算

中图分类号：TP311 文献标识码：A 文章编号：1009-3044（2014）34-8171-03

1 背景

随着互联网的快速发展，软件系统日趋复杂，软件的可靠性、安全性等问题越加突出，潜在的错误可能引发灾难性的后果。因此，如何确保软件系统的正确性和可靠性，并及时发现系统中的错误至关重要。在这方面，形式化验证方法起到了重要作用。

带概率时间自动机以及相关性质的模型检验在工程上具有重要的意义。它保证了实际应用中相关具有概率性为系统例如媒体设备、通信协议等的可靠性、安全性，用于验证具有概率随机行为的系统中事件发生的概率，如“某段时间内，系统出错的概率小于0.05%”、“相应时间内，发送者收到确认的概率大于99.99%”等性质。对于带概率的实时系统的建模，由于概率时间自动机能同时表示概率性、随机性和不确定性，因而在实际中有广泛应用。

2 研究现状

2.1模型检验

模型检验（Model Checking）是一种非常重要的自动化验证技术，它的研究始于二十世纪八十年代初，由Clarke、Emerson[5]等人提出。模型检测最基本的思想就是用状态迁移系统来表达系统行为，用相应的逻辑公式来描述系统规定的性质，这样一来有关“系统是否满足相应的性质需求”就可以转化为一个数学问题如“某个状态迁移系统是否是某个逻辑公式的一个模型”这样一个问题。而对于有穷状态系统，这样的问题是可以判定的，也即在有限时间内可以用计算机程序自动确定。

随后出现的符号模型检验（Symbolic Model Checking）[8]技术使这一方法向实际应用性迈出了关键一步。模型检验已经用在控制系统、通信协议、安全认证协议等方面相应的分析或验证中，取得了很好的成功，影响从学术界扩展到产业界。

2.2概率时间自动机

在计算机科学界，当需要研究计算机的程序设计、体系结构、逻辑操作或者复杂性理论时，自动机作为计算机和计算过程的数学模型经常被用来研究。为了描述实时系统的时间约束，Alur[1]等人提出了时间自动机理论。在表示实时系统的各种数学模型中，时间自动机的影响和应用最为广泛。

时间自动机（Timed Automata）[1]作为有限自动机的时间扩展，在其基础上增加了约束条件和时钟变量，用来作为实时系统的实现模式。时间自动机使用有限个变量来表示时间，称为时间变量；同时用一个约束条件来注释状态转换图，由于这个与时间有关的约束条件决定了状态的转换发生的时间，因此称之为时间限制。对于具有时间行为的系统如实时系统等，时间自动机可以被用来对它们的行为进行分析和建模，相关检查安全性和灵活性等性质的方法在过去二十年间有了很大程度的发展与研究。

作为时间自动机的扩展，概率时间自动机（Probabilistic Timed Automata， PTAs）[7]在马尔可夫决策过程（Markov Decision Processes， MDPs）的基础上加入时钟[9]，是对具有概率、不确定性和实时特性的系统进行建模的工具。

2.3概率时段验算

有关时段演算（Duration Calculus， DC）[12]的研究首先是1989年由周巢尘，Hoare和Raven提出[3]，当时主要有四个演算，即时段演算，扩充时段演算，平均值演算和概率时段演算（Probabilistic Duration Calculus， PDC）[10]。时段演算作为一种实时区间时态逻辑，方法是将布尔函数在某个区间上的积分先进行形式化，然后再用来描述和推导某些离散状态系统的逻辑和实时特性，另外的三个演算都是它的扩展。作为前者的扩展，概率时段演算被用来计算一个以概率时间自动机为模型的系统满足时段演算表达的需求说明的概率。因为系统需求规格实现的满足程度不仅在于其实现功能行为，也依赖于系统中器件的可靠性，概率时段演算正是因此而建立的。

现如今已有算法检验一个时间自动机是否满足以线性时段不变式（Linear Duration Invariants， LDIs）[4]形式表示的时段演算[11]。概率时段演算的相关句法和语义已经给出，但概率时段演算的模型检验算法未给出，这正是本文需要研究的。

2.4 相关验证工具

从有关时间自动机的概念被Alur等人提出之后，许多模型验证工具也陆续出现，用于对实时系统进行建模然后对系统的各种性质来进行验证。以嵌入式系统为例，无论是通信多媒体设备或是自动化控制系统，都需在时间约束下进行，现已有UPPAAL[2]等时间自动机验证工具。该工具使用时间自动机对实时系统来建模和分析验证，不仅具有友好的用户接口，同时也可以图形化地创建时间自动机的模型，或者描述某个规格说明，然后图形化地输出系统的验证结果。另外，很多实时系统也表现出随机行为和不确定性，如由组建失灵、不可靠通信媒体等，现已有PRISM[6]等概率验证工具。

3 模型检验

3.1 主要步骤

对于具有概率性、随机性和不确定性等特征的实时系统，运用概率时间自动机对系统的行为进行数学建模；面向系统规格说明要求的性质时，使用概率时段演算来描述；然后构造一种算法来验证所构造的概率自动机是否满足概率时段演算中的概率线性时段不变式（Probabilistic Linear Duration Invariants， PLDIs）性质，并运用相关自动化验证工具如UPPAAL或PRISM等来验证。endprint

模型检验主要步骤如下：

1）对于具有概率性、不确定性和实时特征的系统，根据系统的规格说明设计，运用相关数学建模工具，对系统的行为进行建模；

2）在实时系统中，使用一种形式化语言，依照系统相关的规格说明准确描述系统要求的性质，例如概率性、不确定性等；

3）构造一种算法，检验建立的系统模型是否满足形式化语言描述的系统属性（图1）；

4）运用相关验证工具完成模型检验的自动化验证。

由于本文研究的是基于概率时间自动机的概率线性时段不变式的模型检验，因而将以上的主要步骤具体化（图3）为：

1）对于带概率等特性的实时系统，本课题采用概率时间自动机对其进行建模。概率时间自动机是马尔可夫决策过程的扩展，可用于描述系统连续时间、带概率行为和不确定选择等特性，在实际中有广泛运用；

2）本课题采用概率时段演算来作为带概率实时系统规格说明的形式化语言，特别是针对概率性这一属性，运用概率时段演算中的概率线性时段不变式来形式化描述；

3）运用模型检验技术，构造算法来分析和验证相关实时系统的概率时间自动机模型和概率时段演算逻辑，检验系统模型是否满足系统要求的属性（图2）；

4）最后使用UPPAAL或PRISM等相关自动化验证工具，验证模型检验算法的正确性，完成系统的验证。

3.2 核心算法

事实上，整个模型检验过程中，最重要的即是模型检验算法（Model Checking Algorithm）。也就是说，如何验证基于某个带概率等性质的实时系统所建模出来的概率时间自动机满足某些用概率时段演算来形式化描述的带概率的性质。

本文采用的方法是根据对概率时间自动机的解析以及对概率时段演算的转化，以此来进一步构造模型检验算法。

首先，针对概率时间自动机（Probabilistic Timed Automata， PTA），该文将其先转换为概率时间结构（Probabilistic Timed Structure， PTS），然后再将概率时间结构转换为区域图（Region Graph）来表示，值得一提的是后者与马尔科夫决策过程（Markov Decision Processes， MDPs）有非常大的关联。具体过程见图4。

其次，针对概率线性时段不变式（Probabilistic Linear Duration Invariants， PLDIs），该文提出的想法是首先将其转换为概率时间计算树逻辑（Probabilistic Timed Computation Tree Logic， PTCTL），然后再将概率时间计算树逻辑转换为概率分支时间逻辑（Probabilistic Branching Time Logic， PBTL）。具体过程见图5。

通过以上两个方法分别将概率时间自动机转换为区域图，将概率线性时段不变式转换为概率分支时间逻辑之后，那么本文所需要证明的基于概率时间自动机的概率线性时段不变式的模型检验算法，就可以转换为证明基于区域图的概率分支时间逻辑的模型检验算法，而后者的证明已经在Kwiatkowska等人的相关论文[7]中给出。具体过程见图6。

4 结束语

本文重点在于基于概率时间自动机的概率时段演算的模型验证算法。之前已有学者研究出算法来检验一个时间自动机是否满足时段演算中的线性时段不变式，该文将其扩展到检查一个概率时间自动机是否满足概率时段演算中的概率线性时段不变式，也就是在实时系统中加入概率特性后的自动化验证。

从工程应用的角度上说，概率时间自动机以及相关性质的模型检验在工程上具有重要的意义。它保证了实际应用中相关具有概率性为系统例如媒体设备、通信协议等的可靠性、安全性，用于验证具有概率随机行为的系统中事件发生的概率。

参考文献：

[1] Alur，Rajeev，David L Dill.A theory of timed automata[J].Theoretical computer science， 1994，126（2）： 183-235.

[2] Behrmann G，David A，Larsen K G.A tutorial on uppaal[M].Formal methods for the design of real-time systems，Springer Berlin Heidelberg，2004：200-236.

[3] Zhou Chaochen，Charles Anthony Richard Hoare，Anders P Ravn.A calculus of durations[J].Information processing letters， 1991，40（5）：269-276.

[4] Chaochen Z，Jingzhong Z，Lu Y，et，al. Linear duration invariants[M].In Formal Techniques in Real-Time and Fault-Tolerant systems，Springer Berlin Heidelberg， 1994： 86-109.

[5] Clarke E M，Emerson E A，Sistla A P.Automatic verification of finite-state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems （TOPLAS），1986，8（2）： 244-263.endprint

[6] Kwiatkowska M，Norman G，Parker D.PRISM 4.0：Verification of probabilistic real-time systems[C].Computer Aided Verification，Springer Berlin Heidelberg，2011： 585-591.

[7] Kwiatkowska M，Norman G，Segala R，et al.Automatic verification of real-time systems with discrete probability distributions[J].Theoretical Computer Science， 2002，282（1）：101-150.

[8] Kwiatkowska M，Norman G，Sproston J，et al.Symbolic model checking for probabilistic timed automata[J]. Information and Computation，2007，205（7）：1027-1077.

[9] Kwiatkowska M，Norman G，Parker D，et al.Performance analysis of probabilistic timed automata using digital clocks[J].Formal Methods in System Design，2006，29（1）：33-78.

[10] Van Hung Dang，Zhou Chaochen.Probabilistic duration calculus for continuous time[J].Formal Aspects of Computing， 1999，11：21-44.

[11] Zhang M，Liu Z，Zhan N.Model checking linear duration invariants of networks of automata[M].Fundamentals of Software Engineering，Springer Berlin Heidelberg，2010：244-259.

[12] Zhou Chaochen，Michael R Hansen.Duration Calculus： A formal approach to real-time systems[M]. Springer，2004.endprint