吳敏

摘要：在實(shí)際工程應(yīng)用中，越來(lái)越多的系統(tǒng)表現(xiàn)出具有概率性等特征。作為對(duì)于此類(lèi)實(shí)時(shí)系統(tǒng)的建模，概率時(shí)間自動(dòng)機(jī)因?yàn)槠淠芡瑫r(shí)表示概率性、隨機(jī)性和不確定性而被廣泛采用。在對(duì)此類(lèi)帶概率性質(zhì)的實(shí)時(shí)系統(tǒng)進(jìn)行描述時(shí)，作為時(shí)段演算的一種擴(kuò)展，概率時(shí)段演算被用來(lái)計(jì)算此類(lèi)系統(tǒng)滿(mǎn)足需求的概率。該文主要概述基于概率時(shí)間自動(dòng)機(jī)的概率時(shí)段演算的模型檢驗(yàn)主要步驟及其核心算法，其中模型檢驗(yàn)的核心算法通過(guò)分別將前兩者轉(zhuǎn)換為區(qū)域圖和概率分支時(shí)間邏輯來(lái)達(dá)成。

關(guān)鍵詞：實(shí)時(shí)系統(tǒng)；模型檢驗(yàn)；概率時(shí)間自動(dòng)機(jī)；概率時(shí)段演算

中圖分類(lèi)號(hào)：TP311 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1009-3044（2014）34-8171-03

1 背景

隨著互聯(lián)網(wǎng)的快速發(fā)展，軟件系統(tǒng)日趨復(fù)雜，軟件的可靠性、安全性等問(wèn)題越加突出，潛在的錯(cuò)誤可能引發(fā)災(zāi)難性的后果。因此，如何確保軟件系統(tǒng)的正確性和可靠性，并及時(shí)發(fā)現(xiàn)系統(tǒng)中的錯(cuò)誤至關(guān)重要。在這方面，形式化驗(yàn)證方法起到了重要作用。

帶概率時(shí)間自動(dòng)機(jī)以及相關(guān)性質(zhì)的模型檢驗(yàn)在工程上具有重要的意義。它保證了實(shí)際應(yīng)用中相關(guān)具有概率性為系統(tǒng)例如媒體設(shè)備、通信協(xié)議等的可靠性、安全性，用于驗(yàn)證具有概率隨機(jī)行為的系統(tǒng)中事件發(fā)生的概率，如“某段時(shí)間內(nèi)，系統(tǒng)出錯(cuò)的概率小于0.05%”、“相應(yīng)時(shí)間內(nèi)，發(fā)送者收到確認(rèn)的概率大于99.99%”等性質(zhì)。對(duì)于帶概率的實(shí)時(shí)系統(tǒng)的建模，由于概率時(shí)間自動(dòng)機(jī)能同時(shí)表示概率性、隨機(jī)性和不確定性，因而在實(shí)際中有廣泛應(yīng)用。

2 研究現(xiàn)狀

2.1模型檢驗(yàn)

模型檢驗(yàn)（Model Checking）是一種非常重要的自動(dòng)化驗(yàn)證技術(shù)，它的研究始于二十世紀(jì)八十年代初，由Clarke、Emerson[5]等人提出。模型檢測(cè)最基本的思想就是用狀態(tài)遷移系統(tǒng)來(lái)表達(dá)系統(tǒng)行為，用相應(yīng)的邏輯公式來(lái)描述系統(tǒng)規(guī)定的性質(zhì)，這樣一來(lái)有關(guān)“系統(tǒng)是否滿(mǎn)足相應(yīng)的性質(zhì)需求”就可以轉(zhuǎn)化為一個(gè)數(shù)學(xué)問(wèn)題如“某個(gè)狀態(tài)遷移系統(tǒng)是否是某個(gè)邏輯公式的一個(gè)模型”這樣一個(gè)問(wèn)題。而對(duì)于有窮狀態(tài)系統(tǒng)，這樣的問(wèn)題是可以判定的，也即在有限時(shí)間內(nèi)可以用計(jì)算機(jī)程序自動(dòng)確定。

隨后出現(xiàn)的符號(hào)模型檢驗(yàn)（Symbolic Model Checking）[8]技術(shù)使這一方法向?qū)嶋H應(yīng)用性邁出了關(guān)鍵一步。模型檢驗(yàn)已經(jīng)用在控制系統(tǒng)、通信協(xié)議、安全認(rèn)證協(xié)議等方面相應(yīng)的分析或驗(yàn)證中，取得了很好的成功，影響從學(xué)術(shù)界擴(kuò)展到產(chǎn)業(yè)界。

2.2概率時(shí)間自動(dòng)機(jī)

在計(jì)算機(jī)科學(xué)界，當(dāng)需要研究計(jì)算機(jī)的程序設(shè)計(jì)、體系結(jié)構(gòu)、邏輯操作或者復(fù)雜性理論時(shí)，自動(dòng)機(jī)作為計(jì)算機(jī)和計(jì)算過(guò)程的數(shù)學(xué)模型經(jīng)常被用來(lái)研究。為了描述實(shí)時(shí)系統(tǒng)的時(shí)間約束，Alur[1]等人提出了時(shí)間自動(dòng)機(jī)理論。在表示實(shí)時(shí)系統(tǒng)的各種數(shù)學(xué)模型中，時(shí)間自動(dòng)機(jī)的影響和應(yīng)用最為廣泛。

時(shí)間自動(dòng)機(jī)（Timed Automata）[1]作為有限自動(dòng)機(jī)的時(shí)間擴(kuò)展，在其基礎(chǔ)上增加了約束條件和時(shí)鐘變量，用來(lái)作為實(shí)時(shí)系統(tǒng)的實(shí)現(xiàn)模式。時(shí)間自動(dòng)機(jī)使用有限個(gè)變量來(lái)表示時(shí)間，稱(chēng)為時(shí)間變量；同時(shí)用一個(gè)約束條件來(lái)注釋狀態(tài)轉(zhuǎn)換圖，由于這個(gè)與時(shí)間有關(guān)的約束條件決定了狀態(tài)的轉(zhuǎn)換發(fā)生的時(shí)間，因此稱(chēng)之為時(shí)間限制。對(duì)于具有時(shí)間行為的系統(tǒng)如實(shí)時(shí)系統(tǒng)等，時(shí)間自動(dòng)機(jī)可以被用來(lái)對(duì)它們的行為進(jìn)行分析和建模，相關(guān)檢查安全性和靈活性等性質(zhì)的方法在過(guò)去二十年間有了很大程度的發(fā)展與研究。

作為時(shí)間自動(dòng)機(jī)的擴(kuò)展，概率時(shí)間自動(dòng)機(jī)（Probabilistic Timed Automata， PTAs）[7]在馬爾可夫決策過(guò)程（Markov Decision Processes， MDPs）的基礎(chǔ)上加入時(shí)鐘[9]，是對(duì)具有概率、不確定性和實(shí)時(shí)特性的系統(tǒng)進(jìn)行建模的工具。

2.3概率時(shí)段驗(yàn)算

有關(guān)時(shí)段演算（Duration Calculus， DC）[12]的研究首先是1989年由周巢塵，Hoare和Raven提出[3]，當(dāng)時(shí)主要有四個(gè)演算，即時(shí)段演算，擴(kuò)充時(shí)段演算，平均值演算和概率時(shí)段演算（Probabilistic Duration Calculus， PDC）[10]。時(shí)段演算作為一種實(shí)時(shí)區(qū)間時(shí)態(tài)邏輯，方法是將布爾函數(shù)在某個(gè)區(qū)間上的積分先進(jìn)行形式化，然后再用來(lái)描述和推導(dǎo)某些離散狀態(tài)系統(tǒng)的邏輯和實(shí)時(shí)特性，另外的三個(gè)演算都是它的擴(kuò)展。作為前者的擴(kuò)展，概率時(shí)段演算被用來(lái)計(jì)算一個(gè)以概率時(shí)間自動(dòng)機(jī)為模型的系統(tǒng)滿(mǎn)足時(shí)段演算表達(dá)的需求說(shuō)明的概率。因?yàn)橄到y(tǒng)需求規(guī)格實(shí)現(xiàn)的滿(mǎn)足程度不僅在于其實(shí)現(xiàn)功能行為，也依賴(lài)于系統(tǒng)中器件的可靠性，概率時(shí)段演算正是因此而建立的。

現(xiàn)如今已有算法檢驗(yàn)一個(gè)時(shí)間自動(dòng)機(jī)是否滿(mǎn)足以線性時(shí)段不變式（Linear Duration Invariants， LDIs）[4]形式表示的時(shí)段演算[11]。概率時(shí)段演算的相關(guān)句法和語(yǔ)義已經(jīng)給出，但概率時(shí)段演算的模型檢驗(yàn)算法未給出，這正是本文需要研究的。

2.4 相關(guān)驗(yàn)證工具

從有關(guān)時(shí)間自動(dòng)機(jī)的概念被Alur等人提出之后，許多模型驗(yàn)證工具也陸續(xù)出現(xiàn)，用于對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行建模然后對(duì)系統(tǒng)的各種性質(zhì)來(lái)進(jìn)行驗(yàn)證。以嵌入式系統(tǒng)為例，無(wú)論是通信多媒體設(shè)備或是自動(dòng)化控制系統(tǒng)，都需在時(shí)間約束下進(jìn)行，現(xiàn)已有UPPAAL[2]等時(shí)間自動(dòng)機(jī)驗(yàn)證工具。該工具使用時(shí)間自動(dòng)機(jī)對(duì)實(shí)時(shí)系統(tǒng)來(lái)建模和分析驗(yàn)證，不僅具有友好的用戶(hù)接口，同時(shí)也可以圖形化地創(chuàng)建時(shí)間自動(dòng)機(jī)的模型，或者描述某個(gè)規(guī)格說(shuō)明，然后圖形化地輸出系統(tǒng)的驗(yàn)證結(jié)果。另外，很多實(shí)時(shí)系統(tǒng)也表現(xiàn)出隨機(jī)行為和不確定性，如由組建失靈、不可靠通信媒體等，現(xiàn)已有PRISM[6]等概率驗(yàn)證工具。

3 模型檢驗(yàn)

3.1 主要步驟

對(duì)于具有概率性、隨機(jī)性和不確定性等特征的實(shí)時(shí)系統(tǒng)，運(yùn)用概率時(shí)間自動(dòng)機(jī)對(duì)系統(tǒng)的行為進(jìn)行數(shù)學(xué)建模；面向系統(tǒng)規(guī)格說(shuō)明要求的性質(zhì)時(shí)，使用概率時(shí)段演算來(lái)描述；然后構(gòu)造一種算法來(lái)驗(yàn)證所構(gòu)造的概率自動(dòng)機(jī)是否滿(mǎn)足概率時(shí)段演算中的概率線性時(shí)段不變式（Probabilistic Linear Duration Invariants， PLDIs）性質(zhì)，并運(yùn)用相關(guān)自動(dòng)化驗(yàn)證工具如UPPAAL或PRISM等來(lái)驗(yàn)證。endprint

模型檢驗(yàn)主要步驟如下：

1） 對(duì)于具有概率性、不確定性和實(shí)時(shí)特征的系統(tǒng)，根據(jù)系統(tǒng)的規(guī)格說(shuō)明設(shè)計(jì)，運(yùn)用相關(guān)數(shù)學(xué)建模工具，對(duì)系統(tǒng)的行為進(jìn)行建模；

2） 在實(shí)時(shí)系統(tǒng)中，使用一種形式化語(yǔ)言，依照系統(tǒng)相關(guān)的規(guī)格說(shuō)明準(zhǔn)確描述系統(tǒng)要求的性質(zhì)，例如概率性、不確定性等；

3） 構(gòu)造一種算法，檢驗(yàn)建立的系統(tǒng)模型是否滿(mǎn)足形式化語(yǔ)言描述的系統(tǒng)屬性（圖1） ；

4）運(yùn)用相關(guān)驗(yàn)證工具完成模型檢驗(yàn)的自動(dòng)化驗(yàn)證。

由于本文研究的是基于概率時(shí)間自動(dòng)機(jī)的概率線性時(shí)段不變式的模型檢驗(yàn)，因而將以上的主要步驟具體化（圖3） 為：

1） 對(duì)于帶概率等特性的實(shí)時(shí)系統(tǒng)，本課題采用概率時(shí)間自動(dòng)機(jī)對(duì)其進(jìn)行建模。概率時(shí)間自動(dòng)機(jī)是馬爾可夫決策過(guò)程的擴(kuò)展，可用于描述系統(tǒng)連續(xù)時(shí)間、帶概率行為和不確定選擇等特性，在實(shí)際中有廣泛運(yùn)用；

2） 本課題采用概率時(shí)段演算來(lái)作為帶概率實(shí)時(shí)系統(tǒng)規(guī)格說(shuō)明的形式化語(yǔ)言，特別是針對(duì)概率性這一屬性，運(yùn)用概率時(shí)段演算中的概率線性時(shí)段不變式來(lái)形式化描述；

3） 運(yùn)用模型檢驗(yàn)技術(shù)，構(gòu)造算法來(lái)分析和驗(yàn)證相關(guān)實(shí)時(shí)系統(tǒng)的概率時(shí)間自動(dòng)機(jī)模型和概率時(shí)段演算邏輯，檢驗(yàn)系統(tǒng)模型是否滿(mǎn)足系統(tǒng)要求的屬性（圖2） ；

4） 最后使用UPPAAL或PRISM等相關(guān)自動(dòng)化驗(yàn)證工具，驗(yàn)證模型檢驗(yàn)算法的正確性，完成系統(tǒng)的驗(yàn)證。

3.2 核心算法

事實(shí)上，整個(gè)模型檢驗(yàn)過(guò)程中，最重要的即是模型檢驗(yàn)算法（Model Checking Algorithm）。也就是說(shuō)，如何驗(yàn)證基于某個(gè)帶概率等性質(zhì)的實(shí)時(shí)系統(tǒng)所建模出來(lái)的概率時(shí)間自動(dòng)機(jī)滿(mǎn)足某些用概率時(shí)段演算來(lái)形式化描述的帶概率的性質(zhì)。

本文采用的方法是根據(jù)對(duì)概率時(shí)間自動(dòng)機(jī)的解析以及對(duì)概率時(shí)段演算的轉(zhuǎn)化，以此來(lái)進(jìn)一步構(gòu)造模型檢驗(yàn)算法。

首先，針對(duì)概率時(shí)間自動(dòng)機(jī)（Probabilistic Timed Automata， PTA），該文將其先轉(zhuǎn)換為概率時(shí)間結(jié)構(gòu)（Probabilistic Timed Structure， PTS），然后再將概率時(shí)間結(jié)構(gòu)轉(zhuǎn)換為區(qū)域圖（Region Graph）來(lái)表示，值得一提的是后者與馬爾科夫決策過(guò)程（Markov Decision Processes， MDPs）有非常大的關(guān)聯(lián)。具體過(guò)程見(jiàn)圖4。

其次，針對(duì)概率線性時(shí)段不變式（Probabilistic Linear Duration Invariants， PLDIs），該文提出的想法是首先將其轉(zhuǎn)換為概率時(shí)間計(jì)算樹(shù)邏輯（Probabilistic Timed Computation Tree Logic， PTCTL），然后再將概率時(shí)間計(jì)算樹(shù)邏輯轉(zhuǎn)換為概率分支時(shí)間邏輯（Probabilistic Branching Time Logic， PBTL）。具體過(guò)程見(jiàn)圖5。

通過(guò)以上兩個(gè)方法分別將概率時(shí)間自動(dòng)機(jī)轉(zhuǎn)換為區(qū)域圖，將概率線性時(shí)段不變式轉(zhuǎn)換為概率分支時(shí)間邏輯之后，那么本文所需要證明的基于概率時(shí)間自動(dòng)機(jī)的概率線性時(shí)段不變式的模型檢驗(yàn)算法，就可以轉(zhuǎn)換為證明基于區(qū)域圖的概率分支時(shí)間邏輯的模型檢驗(yàn)算法，而后者的證明已經(jīng)在Kwiatkowska等人的相關(guān)論文[7]中給出。具體過(guò)程見(jiàn)圖6。

4 結(jié)束語(yǔ)

本文重點(diǎn)在于基于概率時(shí)間自動(dòng)機(jī)的概率時(shí)段演算的模型驗(yàn)證算法。之前已有學(xué)者研究出算法來(lái)檢驗(yàn)一個(gè)時(shí)間自動(dòng)機(jī)是否滿(mǎn)足時(shí)段演算中的線性時(shí)段不變式，該文將其擴(kuò)展到檢查一個(gè)概率時(shí)間自動(dòng)機(jī)是否滿(mǎn)足概率時(shí)段演算中的概率線性時(shí)段不變式，也就是在實(shí)時(shí)系統(tǒng)中加入概率特性后的自動(dòng)化驗(yàn)證。

從工程應(yīng)用的角度上說(shuō)，概率時(shí)間自動(dòng)機(jī)以及相關(guān)性質(zhì)的模型檢驗(yàn)在工程上具有重要的意義。它保證了實(shí)際應(yīng)用中相關(guān)具有概率性為系統(tǒng)例如媒體設(shè)備、通信協(xié)議等的可靠性、安全性，用于驗(yàn)證具有概率隨機(jī)行為的系統(tǒng)中事件發(fā)生的概率。

參考文獻(xiàn)：

[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

[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

[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