概率線性時段不變式的統(tǒng)計模型檢驗
2014-11-19 00:37:55安杰
電腦知識與技術(shù) 2014年30期
摘要：模型檢驗是軟件工程形式化方法的一個重要組成部分，線性時段不變式是形式化方法中表述系統(tǒng)性質(zhì)的一種重要表達式。對線性時段不變式的模型檢驗一直是形式化方法研究的一個重要內(nèi)容。該文提出了一種針對帶概率的線性時段不變式的模型檢驗方法，該方法針對不帶有不確定性的概率模型，運用統(tǒng)計模型檢驗的方法，基于UPPAAL工具實現(xiàn)了概率線性時段不變式的統(tǒng)計模型檢驗。
關(guān)鍵詞：模型檢驗；時段驗算；UPPAAL；概率線性時段不變式
中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2014）30-7097-03
隨著計算機技術(shù)的飛速發(fā)展，計算機系統(tǒng)的規(guī)模和復雜性急劇增加，系統(tǒng)出錯的概率隨之增大。在一些重要的實時系統(tǒng)中，如航空交管、核電站監(jiān)控等，任何錯誤都可能造成重大的經(jīng)濟損失和人員傷亡。如何在系統(tǒng)開發(fā)早期階段驗證設(shè)計的正確性，成為研究人員面對的重要問題。形式化方法（Formal Methods）是重要的提高系統(tǒng)可靠性和安全性的方法。模型檢驗（Model Checking）是形式化方法的重要組成部分。它是一種自動驗證有窮狀態(tài)系統(tǒng)的技術(shù)，通過窮舉搜索狀態(tài)空間來判斷系統(tǒng)是否滿足規(guī)約。時段驗算（Duration Calculus）[1]是周巢塵院士提出的一種區(qū)間時態(tài)邏輯，用于描述系統(tǒng)的區(qū)間性質(zhì)。線性時段不變式是時段驗算性質(zhì)的子集。
本文提出了對于一些概率系統(tǒng)，針對由概率線性時段不變式描述的系統(tǒng)性質(zhì)的統(tǒng)計模型檢驗方法。該方法主要基于模型檢驗工具UPPAAL完成。主要思想是將概率線性時段不變式轉(zhuǎn)化成概率計算樹邏輯（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型檢驗。主要方法是在原自動機模型的基礎(chǔ)上，引入輔助自動機，通過輔助自動機完成線性時段不變式的計算，由UPPAAL完成概率計算。
1 概率線性時段不變式
線性時段不變式（Linear duration invariants， LDI）是一類重要的時段演算公式，由周巢塵等人于1994年首次提出，實時系統(tǒng)中的許多安全性質(zhì)都可以用這類公式進行描述。ProCos項目中的一個著名研究實例[29]就是對煤氣燃燒器的需求進行形式化表述，比如對于需求——“如果對煤氣燃燒器的觀察時長l大于等于60秒，則燃氣泄露時長不會超過整個觀察時長的二十分之一”，就可以使用線性時段不變式來形式化地規(guī)約：
這里的leak是一個布爾函數(shù)，它表示煤氣燃燒器是否處于漏氣狀態(tài)。注意，這里對該煤氣燃燒器的觀察是一個封閉區(qū)間。
然而，在實際情況下系統(tǒng)的行為往往是帶有概率的。比如圖1這樣一個實際系統(tǒng)[3]。開始時，系統(tǒng)在狀態(tài)s1，處于漏氣狀態(tài)，在該狀態(tài)下它有兩個選擇，第一個選擇是到達狀態(tài)s2，第二個選擇是到達狀態(tài)s3，概率分別是0.2和0.8。在狀態(tài)s2和s3 它們分別可以遷移到狀態(tài)s3和s2，概率都是1。
對于這樣的系統(tǒng)，線性時段不變式是否成立就會有一個概率值。
2 概率線性時段不變式的驗證思路
給定由n個作為系統(tǒng)組件的時間自動機A1，A2，...，An構(gòu)成的網(wǎng)絡(luò)A=（L，s0，∑，X，I，E），以及線性時段不變式D，構(gòu)造一個驗證算法，來判斷A是否滿足D。[4]
只要限定D的前件中的a、b為整數(shù)（包含b為?的情形），則D就是可離散化性質(zhì)。那么，只需檢驗A的所有整數(shù)行為對D的滿足性，就可得知A的所有行為對D的滿足性。所以，本節(jié)中規(guī)定，所有組件自動機都是整數(shù)時間自動機。
接著，簡要描述驗證過程的基本步驟：
1） 將每個組件自動機Ai改造成一個新的時間自動機gi。這種改造是為了標記系統(tǒng)A是否處于某個特定位置，能夠幫助計算系統(tǒng)駐留該位置的時長；
2） 構(gòu)造輔助驗證的時間自動機S。在S中，引入兩個變量gc和d，gc用于計算對于A的觀察時長，d用于計算[（D）]的值；
3） 要求S與A并行執(zhí)行，只要觀察時長滿足時限約束（即D的前件），則S會在觀察中的每個整數(shù)時刻檢驗A對D的滿足性。
4） 定義一個CTL公式
輔助自動機S如圖2所示，其中，
· S有3個狀態(tài)：初始狀態(tài)，p0和p1。p0和p1上的約束均為x | 1；
· S有4條邊：一條從初始狀態(tài)連向p0的邊，執(zhí)行賦值語句x=1，使得驗證最早能從0時刻開始；一條從p0連向p1的邊，將變量gc和d初始化為0，用于在觀察開始的瞬間檢驗D的真假；一條從p0連向自身的邊，從A運行后一直保持空轉(zhuǎn)，直至某時刻對A的觀察正式開始才停止執(zhí)行，而執(zhí)行從p0至p1的邊，使得觀察能從A的任意可達狀態(tài)開始；剩余一條從p1連向自身的邊，它會執(zhí)行驗證函數(shù)accum（），用于實時更新gc和d的值；
· S有1個本地時鐘：x，一旦其值累計至1就重置為0，表示只在整數(shù)時刻檢驗D的真假。
3 具體實驗及分析
在試驗中，我們針對圖1中所描述的系統(tǒng)，在UPPAAL中景行具體實驗。圖3和圖4分別是圖1
中描述系統(tǒng)在UPPAAL中的模型以及統(tǒng)計模型檢驗得到的結(jié)果。
可以從結(jié)果中看出，對于圖1中描述的系統(tǒng)，對于帶概率的線性時段表達式的置信區(qū)間是[0.902606，1] 置信度為0.95。
4 結(jié)論
本文通過引入輔助自動機來完成對線性時段不變式的計算，基于UPPAAL完成了帶概率的線性時段不變式的統(tǒng)計模型檢驗。
參考文獻：
[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.
摘要：模型檢驗是軟件工程形式化方法的一個重要組成部分，線性時段不變式是形式化方法中表述系統(tǒng)性質(zhì)的一種重要表達式。對線性時段不變式的模型檢驗一直是形式化方法研究的一個重要內(nèi)容。該文提出了一種針對帶概率的線性時段不變式的模型檢驗方法，該方法針對不帶有不確定性的概率模型，運用統(tǒng)計模型檢驗的方法，基于UPPAAL工具實現(xiàn)了概率線性時段不變式的統(tǒng)計模型檢驗。
關(guān)鍵詞：模型檢驗；時段驗算；UPPAAL；概率線性時段不變式
中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2014）30-7097-03
隨著計算機技術(shù)的飛速發(fā)展，計算機系統(tǒng)的規(guī)模和復雜性急劇增加，系統(tǒng)出錯的概率隨之增大。在一些重要的實時系統(tǒng)中，如航空交管、核電站監(jiān)控等，任何錯誤都可能造成重大的經(jīng)濟損失和人員傷亡。如何在系統(tǒng)開發(fā)早期階段驗證設(shè)計的正確性，成為研究人員面對的重要問題。形式化方法（Formal Methods）是重要的提高系統(tǒng)可靠性和安全性的方法。模型檢驗（Model Checking）是形式化方法的重要組成部分。它是一種自動驗證有窮狀態(tài)系統(tǒng)的技術(shù)，通過窮舉搜索狀態(tài)空間來判斷系統(tǒng)是否滿足規(guī)約。時段驗算（Duration Calculus）[1]是周巢塵院士提出的一種區(qū)間時態(tài)邏輯，用于描述系統(tǒng)的區(qū)間性質(zhì)。線性時段不變式是時段驗算性質(zhì)的子集。
本文提出了對于一些概率系統(tǒng)，針對由概率線性時段不變式描述的系統(tǒng)性質(zhì)的統(tǒng)計模型檢驗方法。該方法主要基于模型檢驗工具UPPAAL完成。主要思想是將概率線性時段不變式轉(zhuǎn)化成概率計算樹邏輯（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型檢驗。主要方法是在原自動機模型的基礎(chǔ)上，引入輔助自動機，通過輔助自動機完成線性時段不變式的計算，由UPPAAL完成概率計算。
1 概率線性時段不變式
線性時段不變式（Linear duration invariants， LDI）是一類重要的時段演算公式，由周巢塵等人于1994年首次提出，實時系統(tǒng)中的許多安全性質(zhì)都可以用這類公式進行描述。ProCos項目中的一個著名研究實例[29]就是對煤氣燃燒器的需求進行形式化表述，比如對于需求——“如果對煤氣燃燒器的觀察時長l大于等于60秒，則燃氣泄露時長不會超過整個觀察時長的二十分之一”，就可以使用線性時段不變式來形式化地規(guī)約：
這里的leak是一個布爾函數(shù)，它表示煤氣燃燒器是否處于漏氣狀態(tài)。注意，這里對該煤氣燃燒器的觀察是一個封閉區(qū)間。
然而，在實際情況下系統(tǒng)的行為往往是帶有概率的。比如圖1這樣一個實際系統(tǒng)[3]。開始時，系統(tǒng)在狀態(tài)s1，處于漏氣狀態(tài)，在該狀態(tài)下它有兩個選擇，第一個選擇是到達狀態(tài)s2，第二個選擇是到達狀態(tài)s3，概率分別是0.2和0.8。在狀態(tài)s2和s3 它們分別可以遷移到狀態(tài)s3和s2，概率都是1。
對于這樣的系統(tǒng)，線性時段不變式是否成立就會有一個概率值。
2 概率線性時段不變式的驗證思路
給定由n個作為系統(tǒng)組件的時間自動機A1，A2，...，An構(gòu)成的網(wǎng)絡(luò)A=（L，s0，∑，X，I，E），以及線性時段不變式D，構(gòu)造一個驗證算法，來判斷A是否滿足D。[4]
只要限定D的前件中的a、b為整數(shù)（包含b為?的情形），則D就是可離散化性質(zhì)。那么，只需檢驗A的所有整數(shù)行為對D的滿足性，就可得知A的所有行為對D的滿足性。所以，本節(jié)中規(guī)定，所有組件自動機都是整數(shù)時間自動機。
接著，簡要描述驗證過程的基本步驟：
1） 將每個組件自動機Ai改造成一個新的時間自動機gi。這種改造是為了標記系統(tǒng)A是否處于某個特定位置，能夠幫助計算系統(tǒng)駐留該位置的時長；
2） 構(gòu)造輔助驗證的時間自動機S。在S中，引入兩個變量gc和d，gc用于計算對于A的觀察時長，d用于計算[（D）]的值；
3） 要求S與A并行執(zhí)行，只要觀察時長滿足時限約束（即D的前件），則S會在觀察中的每個整數(shù)時刻檢驗A對D的滿足性。
4） 定義一個CTL公式
輔助自動機S如圖2所示，其中，
· S有3個狀態(tài)：初始狀態(tài)，p0和p1。p0和p1上的約束均為x | 1；
· S有4條邊：一條從初始狀態(tài)連向p0的邊，執(zhí)行賦值語句x=1，使得驗證最早能從0時刻開始；一條從p0連向p1的邊，將變量gc和d初始化為0，用于在觀察開始的瞬間檢驗D的真假；一條從p0連向自身的邊，從A運行后一直保持空轉(zhuǎn)，直至某時刻對A的觀察正式開始才停止執(zhí)行，而執(zhí)行從p0至p1的邊，使得觀察能從A的任意可達狀態(tài)開始；剩余一條從p1連向自身的邊，它會執(zhí)行驗證函數(shù)accum（），用于實時更新gc和d的值；
· S有1個本地時鐘：x，一旦其值累計至1就重置為0，表示只在整數(shù)時刻檢驗D的真假。
3 具體實驗及分析
在試驗中，我們針對圖1中所描述的系統(tǒng)，在UPPAAL中景行具體實驗。圖3和圖4分別是圖1
中描述系統(tǒng)在UPPAAL中的模型以及統(tǒng)計模型檢驗得到的結(jié)果。
可以從結(jié)果中看出，對于圖1中描述的系統(tǒng)，對于帶概率的線性時段表達式的置信區(qū)間是[0.902606，1] 置信度為0.95。
4 結(jié)論
本文通過引入輔助自動機來完成對線性時段不變式的計算，基于UPPAAL完成了帶概率的線性時段不變式的統(tǒng)計模型檢驗。
參考文獻：
[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.
摘要：模型檢驗是軟件工程形式化方法的一個重要組成部分，線性時段不變式是形式化方法中表述系統(tǒng)性質(zhì)的一種重要表達式。對線性時段不變式的模型檢驗一直是形式化方法研究的一個重要內(nèi)容。該文提出了一種針對帶概率的線性時段不變式的模型檢驗方法，該方法針對不帶有不確定性的概率模型，運用統(tǒng)計模型檢驗的方法，基于UPPAAL工具實現(xiàn)了概率線性時段不變式的統(tǒng)計模型檢驗。
關(guān)鍵詞：模型檢驗；時段驗算；UPPAAL；概率線性時段不變式
中圖分類號：TP311 文獻標識碼：A 文章編號：1009-3044（2014）30-7097-03
隨著計算機技術(shù)的飛速發(fā)展，計算機系統(tǒng)的規(guī)模和復雜性急劇增加，系統(tǒng)出錯的概率隨之增大。在一些重要的實時系統(tǒng)中，如航空交管、核電站監(jiān)控等，任何錯誤都可能造成重大的經(jīng)濟損失和人員傷亡。如何在系統(tǒng)開發(fā)早期階段驗證設(shè)計的正確性，成為研究人員面對的重要問題。形式化方法（Formal Methods）是重要的提高系統(tǒng)可靠性和安全性的方法。模型檢驗（Model Checking）是形式化方法的重要組成部分。它是一種自動驗證有窮狀態(tài)系統(tǒng)的技術(shù)，通過窮舉搜索狀態(tài)空間來判斷系統(tǒng)是否滿足規(guī)約。時段驗算（Duration Calculus）[1]是周巢塵院士提出的一種區(qū)間時態(tài)邏輯，用于描述系統(tǒng)的區(qū)間性質(zhì)。線性時段不變式是時段驗算性質(zhì)的子集。
本文提出了對于一些概率系統(tǒng)，針對由概率線性時段不變式描述的系統(tǒng)性質(zhì)的統(tǒng)計模型檢驗方法。該方法主要基于模型檢驗工具UPPAAL完成。主要思想是將概率線性時段不變式轉(zhuǎn)化成概率計算樹邏輯（Probabilistic Computing Tree Logic）[2]，然后由UPPAAL完成模型檢驗。主要方法是在原自動機模型的基礎(chǔ)上，引入輔助自動機，通過輔助自動機完成線性時段不變式的計算，由UPPAAL完成概率計算。
1 概率線性時段不變式
線性時段不變式（Linear duration invariants， LDI）是一類重要的時段演算公式，由周巢塵等人于1994年首次提出，實時系統(tǒng)中的許多安全性質(zhì)都可以用這類公式進行描述。ProCos項目中的一個著名研究實例[29]就是對煤氣燃燒器的需求進行形式化表述，比如對于需求——“如果對煤氣燃燒器的觀察時長l大于等于60秒，則燃氣泄露時長不會超過整個觀察時長的二十分之一”，就可以使用線性時段不變式來形式化地規(guī)約：
這里的leak是一個布爾函數(shù)，它表示煤氣燃燒器是否處于漏氣狀態(tài)。注意，這里對該煤氣燃燒器的觀察是一個封閉區(qū)間。
然而，在實際情況下系統(tǒng)的行為往往是帶有概率的。比如圖1這樣一個實際系統(tǒng)[3]。開始時，系統(tǒng)在狀態(tài)s1，處于漏氣狀態(tài)，在該狀態(tài)下它有兩個選擇，第一個選擇是到達狀態(tài)s2，第二個選擇是到達狀態(tài)s3，概率分別是0.2和0.8。在狀態(tài)s2和s3 它們分別可以遷移到狀態(tài)s3和s2，概率都是1。
對于這樣的系統(tǒng)，線性時段不變式是否成立就會有一個概率值。
2 概率線性時段不變式的驗證思路
給定由n個作為系統(tǒng)組件的時間自動機A1，A2，...，An構(gòu)成的網(wǎng)絡(luò)A=（L，s0，∑，X，I，E），以及線性時段不變式D，構(gòu)造一個驗證算法，來判斷A是否滿足D。[4]
只要限定D的前件中的a、b為整數(shù)（包含b為?的情形），則D就是可離散化性質(zhì)。那么，只需檢驗A的所有整數(shù)行為對D的滿足性，就可得知A的所有行為對D的滿足性。所以，本節(jié)中規(guī)定，所有組件自動機都是整數(shù)時間自動機。
接著，簡要描述驗證過程的基本步驟：
1） 將每個組件自動機Ai改造成一個新的時間自動機gi。這種改造是為了標記系統(tǒng)A是否處于某個特定位置，能夠幫助計算系統(tǒng)駐留該位置的時長；
2） 構(gòu)造輔助驗證的時間自動機S。在S中，引入兩個變量gc和d，gc用于計算對于A的觀察時長，d用于計算[（D）]的值；
3） 要求S與A并行執(zhí)行，只要觀察時長滿足時限約束（即D的前件），則S會在觀察中的每個整數(shù)時刻檢驗A對D的滿足性。
4） 定義一個CTL公式
輔助自動機S如圖2所示，其中，
· S有3個狀態(tài)：初始狀態(tài)，p0和p1。p0和p1上的約束均為x | 1；
· S有4條邊：一條從初始狀態(tài)連向p0的邊，執(zhí)行賦值語句x=1，使得驗證最早能從0時刻開始；一條從p0連向p1的邊，將變量gc和d初始化為0，用于在觀察開始的瞬間檢驗D的真假；一條從p0連向自身的邊，從A運行后一直保持空轉(zhuǎn)，直至某時刻對A的觀察正式開始才停止執(zhí)行，而執(zhí)行從p0至p1的邊，使得觀察能從A的任意可達狀態(tài)開始；剩余一條從p1連向自身的邊，它會執(zhí)行驗證函數(shù)accum（），用于實時更新gc和d的值；
· S有1個本地時鐘：x，一旦其值累計至1就重置為0，表示只在整數(shù)時刻檢驗D的真假。
3 具體實驗及分析
在試驗中，我們針對圖1中所描述的系統(tǒng)，在UPPAAL中景行具體實驗。圖3和圖4分別是圖1
中描述系統(tǒng)在UPPAAL中的模型以及統(tǒng)計模型檢驗得到的結(jié)果。
可以從結(jié)果中看出，對于圖1中描述的系統(tǒng)，對于帶概率的線性時段表達式的置信區(qū)間是[0.902606，1] 置信度為0.95。
4 結(jié)論
本文通過引入輔助自動機來完成對線性時段不變式的計算，基于UPPAAL完成了帶概率的線性時段不變式的統(tǒng)計模型檢驗。
參考文獻：
[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.
