張　坤，葉俊民，王　嬙，趙麗嫻，陳　曙

（華中師范大學(xué)　　計(jì)算機(jī)學(xué)院，武漢　430079）

基于活性順序圖的形式化驗(yàn)證方法及工具研究

張坤，葉俊民，王嬙，趙麗嫻，陳曙

（華中師范大學(xué)計(jì)算機(jī)學(xué)院，武漢430079）

近年來，形式化驗(yàn)證方法在軟件開發(fā)過程的作用越來越大；如何充分利用形式化驗(yàn)證方法提高軟件系統(tǒng)的可靠性已成為軟件開發(fā)者及使用者主要關(guān)注的問題；總結(jié)了近年來基于活性順序圖的形式化驗(yàn)證方法的研究進(jìn)展，首先介紹活性順序圖的語言及其表達(dá)能力與復(fù)雜性，然后深入分析現(xiàn)有的基于活性順序圖的形式化驗(yàn)證的關(guān)鍵技術(shù)及其典型應(yīng)用，最后實(shí)現(xiàn)一種基于活性順序圖的運(yùn)行時(shí)驗(yàn)證工具，實(shí)驗(yàn)證明使用本驗(yàn)證工具進(jìn)行形式化驗(yàn)證的可行性。

活性順序圖；形式化驗(yàn)證；軟件開發(fā)過程

0　引言

隨著計(jì)算機(jī)技術(shù)的發(fā)展，軟件系統(tǒng)已經(jīng)滲透到人們的生活之中，軟件系統(tǒng)關(guān)系著人民的信息安全、財(cái)產(chǎn)安全乃至生命安全。形式化驗(yàn)證方法在軟件開發(fā)過程中的作用越來越受到軟件開發(fā)者的重視，確保軟件系統(tǒng)在任何時(shí)候都與需求規(guī)約一致，已經(jīng)成為軟件開發(fā)者及使用者關(guān)注的重要問題，利用場景對系統(tǒng)進(jìn)行建模和分析已成為軟件開發(fā)過程中形式化驗(yàn)證的重要技術(shù)和方法［1］。目前形式化驗(yàn)證方法主要包括模型驗(yàn)證［2］與運(yùn)行時(shí)驗(yàn)證［3］等。

基于場景的形式化驗(yàn)證經(jīng)常使用順序圖對系統(tǒng)進(jìn)行建模和分析，順序圖是一種基于場景的語言，能夠圖形化地表示系統(tǒng)實(shí)例間交互的時(shí)序關(guān)系。順序圖包括消息順序圖（Message Sequence Chart，簡稱MSC）［4］、.0順序圖（UML2.0 Sequence Diagram，簡稱UML-SD）［5］、活性順序圖（Live Sequence Chart，簡稱LSC）［6］及其它變種。MSC由ITU提出并在業(yè)界得到廣泛應(yīng)用，但MSC表達(dá)能力很有限，只能表示可能發(fā)生的場景，不能表示系統(tǒng)必須滿足的場景。雖然UML-SD增加了一些新的操作符，增強(qiáng)了其表達(dá)能力，但UML-SD的非形式化語義也限制了其應(yīng)用。LSC對MSC進(jìn)行擴(kuò)展，LSC使用universal和existential兩種模式區(qū)分強(qiáng)制場景和可能場景，且LSC具有形式化語義。因此，軟件開發(fā)過程中形式化驗(yàn)證經(jīng)常使用LSC描述系統(tǒng)場景中事件交互的時(shí)態(tài)關(guān)系。此外，LSC可以用來建模實(shí)際系統(tǒng)，也可以用于描述場景需求，基于LSC的形式化驗(yàn)證方法不僅使系統(tǒng)需求的行為語義易于理解，而且還能盡早地發(fā)現(xiàn)軟件設(shè)計(jì)錯(cuò)誤。利用LSC對系統(tǒng)進(jìn)行建模和分析已成為需求分析階段的重要技術(shù)和方法。

LSC在MSC的基礎(chǔ)上增加了活性（liveness）的概念，活性表示需求的場景一定會(huì)發(fā)生［7］。LSC分為universal和existential兩種模式，universal圖表示系統(tǒng)一定發(fā)生的場景，用實(shí)線矩形框表示，existential圖表示系統(tǒng)可能發(fā)生的場景，用虛線矩形框表示。universal圖包含一個(gè)前置圖（prechart）和一個(gè)主圖（main chart），前置圖表示觸發(fā)場景，用虛線六邊形表示，主圖表示響應(yīng)場景，用實(shí)線矩形表示，universal圖表示的意思是，如果前置圖表示的觸發(fā)場景成功執(zhí)行了，主圖就必須執(zhí)行。existential圖則只含有主圖，不包含前置圖，existential圖只要求前置圖與主圖的一個(gè)事件實(shí)例，不強(qiáng)制要求主圖要在每一次前置圖執(zhí)行后執(zhí)行。

圖1　universal模式LSC圖

為了描述系統(tǒng)的強(qiáng)制性行為和可能性行為，LSC對圖中所有的位置、消息和條件等元素分配了溫度屬性，若元素的溫度是Hot，則該元素一定會(huì)發(fā)生，若元素的溫度值是Cold，則該元素可能會(huì)發(fā)生。在LSC圖中，Hot用實(shí)線表示，描述系統(tǒng)滿足強(qiáng)制行為；Cold用虛線表示，描述系統(tǒng)可能滿足的行為。如果實(shí)例線上某個(gè)位置是Hot位置，可以直接從當(dāng)前位置移動(dòng)到下一個(gè)Hot位置；如果這個(gè)位置是Cold位置，實(shí)例運(yùn)行可能通過該位置。如果某個(gè)消息溫度值是Hot，則該消息一定會(huì)被發(fā)送與接收；如果消息的溫度值是Cold，表示該消息一定會(huì)被發(fā)送，但是消息可能被接收，也可能不被接收。

1　LSC語言定義

下面基于文獻(xiàn)［8］形式化定義LSC語言，首先定義LSC語法，由于基于LSC的形式化驗(yàn)證過程一般基于程序執(zhí)行軌跡，這里給出LSC基于軌跡的語義。文獻(xiàn)［9］論述LSC具有很強(qiáng)的表達(dá)能力，為了充分使用LSC進(jìn)行形式化驗(yàn)證，有必要對LSC的復(fù)雜性進(jìn)行論述。

1.1LSC語法

令inst（c）表示LSC圖c的實(shí)例線集合，dom（c，i）表示實(shí)例線i上的位置集合，dom（c）表示LSC圖c上位置集合。

定義1（LSC）：LSC定義為一個(gè)7元組L=＜I，dom，ML，SR，Pre，Mode，quant＞，其中：

1）I是實(shí)例線的結(jié)合；

2）Dom是圖c上的位置集合；

3）ML是圖c的消息集合；

4）SR是圖c的同步發(fā)生區(qū)域；

5）Pre是圖c的前置圖，可為空。

6）Mode∈｛initial，invariant，iterative｝，Mode決定LSC的執(zhí)行頻率。

7）quant∈｛universal，existential｝，quant決定LSC的模式。

1.2LSC基于軌跡的語義

由于定義LSC基于軌跡的語義時(shí)要使用LSC的cut，這里首先定義LSC的cut。

定義2（cut［8］）一個(gè)cut指圖中每個(gè)實(shí)例到其位置的一個(gè)映射，cut?dom（c，i0）×...×dom（c，in），其中inst（c）=｛i0，...，in｝。

使用cut，下面定義LSC的執(zhí)行軌跡。

定義3（執(zhí)行軌跡）：令cuts序列c=c0，c1，...，ck為LSC圖c的一次執(zhí)行，執(zhí)行軌跡w=trace（c），則w=w0w1，...，wk。其中c0，wi表示圖c中事件的集合。

一個(gè)LSC的軌跡語言是LSC圖c執(zhí)行所產(chǎn)生的所有執(zhí)行軌跡的集合。Lc=｛w|?（c0，c1，...ck）∈R uns（c）｝，使得w =trace（c0，c1，...，ck），其中Runs（c）表示LSC所有執(zhí)行軌跡的集合。

1.3LSC語言的表達(dá)能力與復(fù)雜性論述

在一定限制條件下，可以將LSC轉(zhuǎn)換為等價(jià)的時(shí)序邏輯語言或者自動(dòng)機(jī)語言［9］，這表明LSC語言具有很強(qiáng)的表達(dá)能力。Bontemps等人［10］主要討論了LSC語言的復(fù)雜性，表明LSC語言復(fù)雜性主要包括兩個(gè)方面：1）LSC語義依賴于偏序關(guān)系；2）LSC的規(guī)約是非結(jié)構(gòu)化的。前者引起的復(fù)雜性可以在實(shí)際應(yīng)用中避免，因?yàn)閷?shí)際應(yīng)用場景一般是線性時(shí)序場景。后者引起的復(fù)雜性問題可以通過額外的信息生成高效的算法來解決。研究表明，LSC轉(zhuǎn)換為時(shí)序邏輯語言或自動(dòng)機(jī)語言的復(fù)雜度相對較小，因此LSC經(jīng)常用于形式化驗(yàn)證。

2　基于LSC的形式化驗(yàn)證方法

在形式化驗(yàn)證過程中，主要有建模系統(tǒng)和描述需求規(guī)約兩類需求。由于LSC可以用來建模系統(tǒng)行為，也可以用于描述場景需求［8］。因此，基于LSC的形式化驗(yàn)證方法關(guān)鍵技術(shù)主要從以下兩個(gè)方面進(jìn)行論述。

2.1使用LSC建模系統(tǒng)行為

形式化驗(yàn)證需要建模系統(tǒng)行為，MSC可以直觀的描述系統(tǒng)中對象間的交互情景，MSC可以解決基于狀態(tài)圖作為系統(tǒng)行為模型的局限性問題，但是在捕獲系統(tǒng)行為需求時(shí)，MSC也存在一些不足［11］，LSC也可以建模眾多系統(tǒng)，且LSC語言可以補(bǔ)充MSC的不足，因此，使用LSC建模系統(tǒng)行為的研究逐漸展開。使用LSC建模系統(tǒng)行為即從基于場景規(guī)約的LSC構(gòu)建可執(zhí)行的系統(tǒng)。目前主要有兩種方法［12］，第一種是自動(dòng)合成系統(tǒng)的方法。給定LSC模型，確定是否存在一個(gè)系統(tǒng)滿足該LSC模型，如果存在這樣的系統(tǒng)，則根據(jù)LSC模型中實(shí)例間的交互確定實(shí)例的有限狀態(tài)機(jī)或狀態(tài)圖，有限狀態(tài)機(jī)或狀態(tài)圖集合構(gòu)成確定滿足該LSC的系統(tǒng)，但是合成的系統(tǒng)要滿足兩個(gè)需求：1）合成的系統(tǒng)需要監(jiān)聽系統(tǒng)中發(fā)生的事件；2）合成的系統(tǒng)必須滿足LSC模型，自動(dòng)合成系統(tǒng)的方法已在文獻(xiàn)［11］實(shí)現(xiàn)。第二種方法是從LSC規(guī)約中場景實(shí)例間的交互建?？蓤?zhí)行的系統(tǒng)［13］，該方法不是為每個(gè)實(shí)例產(chǎn)生實(shí)例的內(nèi)部規(guī)約，而是按照算法直接執(zhí)行場景，在LSC的場景描述中定義可執(zhí)行的系統(tǒng)及系統(tǒng)運(yùn)行產(chǎn)生的狀態(tài)。這種方法有一個(gè)研究成果，即Play-out機(jī)制［13］，Play-out機(jī)制允許工程師與其它相關(guān)人員更好地了解場景實(shí)例交互所產(chǎn)生的行為。

這兩種常見的方法各有特點(diǎn)，兩種方法的比較見表1所列。

2.2使用LSC獲取待驗(yàn)證的系統(tǒng)性質(zhì)

形式化驗(yàn)證經(jīng)常使用時(shí)序邏輯語言或自動(dòng)機(jī)語言等描述系統(tǒng)的待驗(yàn)證性質(zhì)。但在工程應(yīng)用中，尤其是在基于場景的軟件工程中使用時(shí)序邏輯并不實(shí)際。由于LSC語言具有直觀性和形式化的特點(diǎn)，因此在形式化驗(yàn)證中，LSC經(jīng)常作為系統(tǒng)開發(fā)過程中需求規(guī)約描述語言，然后將LSC轉(zhuǎn)換為待驗(yàn)證的性質(zhì)，這些性質(zhì)然后用時(shí)序邏輯語言或自動(dòng)機(jī)語言進(jìn)行描述。關(guān)于從LSC獲取待驗(yàn)證的系統(tǒng)性質(zhì)，下面分LSC轉(zhuǎn)換為時(shí)序邏輯和LSC轉(zhuǎn)換為自動(dòng)機(jī)兩種類型進(jìn)行論述。

表1　使用LSC建模系統(tǒng)的兩種方法比較

2.2.1LSC轉(zhuǎn)換為時(shí)序邏輯

Bontemps等人［14］對于只含LSC核心語法的LSC規(guī)約，證明任何LSC規(guī)約都可以轉(zhuǎn)換為時(shí)序邏輯公式。Kugler等人［15］設(shè)計(jì)算法將LSC轉(zhuǎn)換為LTL公式，其它相關(guān)的研究很多基于該轉(zhuǎn)換算法，文獻(xiàn)［15］主要產(chǎn)生兩種性質(zhì)：圖中消息的偏序性質(zhì)（φ性質(zhì)），圖中消息的唯一性性質(zhì)（χ性質(zhì)）。對于一個(gè)universal圖，對應(yīng)的LTL公式φc形式如下。

該轉(zhuǎn)換等式從上到下分為三部分，頂部的φ性質(zhì)保證了前置圖與主圖中的消息都是偏序關(guān)系，中部保證了只有前置圖的消息都發(fā)生后，主圖中的消息才并且一定發(fā)生，底部保證了圖中的消息只發(fā)生一次。文獻(xiàn)［15］中的轉(zhuǎn)換方法為LSC圖每一個(gè)可能的執(zhí)行入口都生成LTL公式，轉(zhuǎn)換后的LTL公式的規(guī)模是LSC中事件規(guī)模的平方復(fù)雜度。Kumar等人［16］從化簡偏序性性質(zhì)和化簡唯一性性質(zhì)兩個(gè)方面，利用LSC規(guī)約中性質(zhì)的實(shí)現(xiàn)文獻(xiàn)［15］中轉(zhuǎn)換的優(yōu)化，優(yōu)化后所產(chǎn)生時(shí)序邏輯的規(guī)模是主圖中最大消息規(guī)模的平方復(fù)雜度，該優(yōu)化在大多數(shù)情況下可以縮小轉(zhuǎn)換所產(chǎn)生的LTL公式的規(guī)模。

此外，LSC轉(zhuǎn)換為時(shí)序邏輯這些方法有一定的限制，這些方法的研究一般只針對LSC核心語法所表示的需求規(guī)約，缺少將完整LSC語法轉(zhuǎn)換為時(shí)序邏輯的算法。

2.2.2LSC轉(zhuǎn)換為自動(dòng)機(jī)

文獻(xiàn)［17］實(shí)現(xiàn)了LSC轉(zhuǎn)換為自動(dòng)機(jī)，他們將符號化自動(dòng)機(jī)結(jié)構(gòu)形式的LSC圖作為輸入的自動(dòng)機(jī)結(jié)構(gòu)，然后通過增加接受狀態(tài)和增加/更新遷移將符號化自動(dòng)機(jī)結(jié)構(gòu)轉(zhuǎn)換為可以檢測安全與活性錯(cuò)誤的否定自動(dòng)機(jī)。該轉(zhuǎn)換過程關(guān)注于創(chuàng)建自動(dòng)機(jī)結(jié)構(gòu)，并使用得出的自動(dòng)機(jī)實(shí)現(xiàn)形式化驗(yàn)證，如果需求規(guī)約用時(shí)間擴(kuò)展的LSC表示，則可將LSC轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)。一般的轉(zhuǎn)換過程關(guān)注于創(chuàng)建自動(dòng)機(jī)結(jié)構(gòu)，Kumar等人［18］則直接研究了適用于發(fā)現(xiàn)系統(tǒng)錯(cuò)誤的LSC到自動(dòng)機(jī)的轉(zhuǎn)換過程，他們的LSC轉(zhuǎn)換為自動(dòng)機(jī)的轉(zhuǎn)換過程使得性能與可擴(kuò)展性均顯著提升。

將LSC規(guī)約轉(zhuǎn)換為自動(dòng)機(jī)語言，然后使用基于自動(dòng)機(jī)語言進(jìn)行形式化驗(yàn)證，這種方法可以支持LSC的更大語法子集，且支持更大規(guī)模的LSC規(guī)約［17］。

3　基于LSC的形式化驗(yàn)證典型應(yīng)用

基于LSC的形式化驗(yàn)證應(yīng)用已有很多，從形式化驗(yàn)證方法分類來看，目前基于LSC的形式化驗(yàn)證主要應(yīng)用有模型驗(yàn)證領(lǐng)域與運(yùn)行時(shí)驗(yàn)證領(lǐng)域等。下面就基于LSC的形式化驗(yàn)證在模型驗(yàn)證領(lǐng)域與運(yùn)行時(shí)驗(yàn)證領(lǐng)域的應(yīng)用進(jìn)展加以論述。

3.1基于LSC形式化方法的模型檢測

LSC可以作為系統(tǒng)需求規(guī)約描述語言，通過將LSC轉(zhuǎn)換為時(shí)序邏輯語言或自動(dòng)機(jī)語言的方法可以從LSC獲取系統(tǒng)待驗(yàn)證的性質(zhì)［17］。此外，LSC又可以建模系統(tǒng)行為，因此，LSC也是系統(tǒng)的高級編程語言。模型檢測即需要建模系統(tǒng)也需要時(shí)序邏輯或自動(dòng)機(jī)語言等表示的需求規(guī)約，而LSC正好具有上述兩種表述能力。因此，很多模型檢驗(yàn)應(yīng)用研究都基于LSC，基于LSC形式化方法的模型檢驗(yàn)應(yīng)用研究可以分為三類：

1）LSC只轉(zhuǎn)化為系統(tǒng)行為模型，待驗(yàn)證的系統(tǒng)性質(zhì)規(guī)約由用戶定義［17］；

2）系統(tǒng)行為模型由其它模型產(chǎn)生，待驗(yàn)證系統(tǒng)性質(zhì)規(guī)約從LSC中獲?。?9］；

3）系統(tǒng)行為模型由LSC轉(zhuǎn)換形成，待驗(yàn)證系統(tǒng)性質(zhì)規(guī)約也從LSC中獲?。?］。

其中，情形3）的基于LSC形式化方法的模型檢測過程如圖2所示。

圖2　基于LSC形式化方法的模型檢測過程

3.2基于LSC形式化方法的運(yùn)行時(shí)驗(yàn)證

LSC可以轉(zhuǎn)換為時(shí)序邏輯語言或者自動(dòng)機(jī)語言來獲取系統(tǒng)需求規(guī)約，將轉(zhuǎn)換的時(shí)序邏輯語言或者自動(dòng)機(jī)語言表示的需求規(guī)約作為監(jiān)控器［3］，使用運(yùn)行時(shí)驗(yàn)證的相關(guān)技術(shù)［20］就可以實(shí)現(xiàn)基于LSC形式化方法的運(yùn)行時(shí)驗(yàn)證。基于LSC形式化方法的運(yùn)行時(shí)驗(yàn)證過程如圖3所示。

圖3　基于LSC形式化方法的運(yùn)行時(shí)驗(yàn)證過程

基于LSC的形式化方法應(yīng)用于運(yùn)行時(shí)驗(yàn)證領(lǐng)域已經(jīng)有相關(guān)研究，Chai等人［21］提出中標(biāo)準(zhǔn)LSC語言在其研究的嵌入式實(shí)時(shí)系統(tǒng)中表示特定場景的正確性性質(zhì)還不夠充分，因此引入充分前置圖的概念，提出擴(kuò)展的活性順序圖 （extension of live sequence charts，簡稱eLSC），并分為有迭代eLSC和無迭代eLSC兩種場景，有迭代eLSC場景直接使用文獻(xiàn)［15］中的方法轉(zhuǎn)換成為LTL公式，并使用公式重寫的方法使用Maude工具引擎［22］進(jìn)行運(yùn)行時(shí)驗(yàn)證，無迭代eLSC場景則設(shè)置專門的算法進(jìn)行運(yùn)行時(shí)驗(yàn)證。并研究了歐洲列車控制系統(tǒng)（ETCS）中RBC/RBC切換場景，實(shí)現(xiàn)基于LSC形式化方法用于運(yùn)行時(shí)驗(yàn)證。

4　基于LSC的驗(yàn)證工具實(shí)現(xiàn)

本文實(shí)現(xiàn)的基于LSC的驗(yàn)證工具的設(shè)計(jì)思路是：首先，插裝獲取系統(tǒng)執(zhí)行軌跡，導(dǎo)入目標(biāo)系統(tǒng)程序，使用Spring AOP進(jìn)行代碼插裝獲取其執(zhí)行軌跡；然后，輸入使用從LSC轉(zhuǎn)換所得的LTL公式；最后，自動(dòng)生成被驗(yàn)證的項(xiàng)目文件，再調(diào)用Maude工具引擎實(shí)現(xiàn)運(yùn)行時(shí)驗(yàn)證。

4.1工具架構(gòu)

本文設(shè)計(jì)的基于LSC的驗(yàn)證工具架構(gòu)如圖4所示。

圖4　運(yùn)行時(shí)驗(yàn)證工具框架

1）插裝獲取系統(tǒng)執(zhí)行軌跡：

在此模塊中，用戶可以導(dǎo)入要驗(yàn)證的目標(biāo)系統(tǒng)源程序，并且可以在工具中查找已導(dǎo)入的目標(biāo)系統(tǒng)程序代碼。在目標(biāo)系統(tǒng)程序運(yùn)行時(shí)，根據(jù)配置的插裝點(diǎn)通過Spring AOP插裝獲取目標(biāo)系統(tǒng)的執(zhí)行軌跡序列，并將執(zhí)行軌跡序列存貯在本地，便于后續(xù)的運(yùn)行時(shí)驗(yàn)證。

2）導(dǎo)入需求規(guī)約：

在此模塊中，根據(jù)LSC描述的需求規(guī)約場景，用戶可以導(dǎo)入從LSC轉(zhuǎn)換所得的LTL公式，導(dǎo)入的LTL公式作為需求規(guī)約將存貯在本地，便于后續(xù)的運(yùn)行時(shí)驗(yàn)證。

3）運(yùn)行時(shí)驗(yàn)證：

在此模塊中，工具根據(jù)公式重寫算法自動(dòng)生成相應(yīng)的重寫規(guī)則，Maude工具引擎根據(jù)重寫規(guī)則文件運(yùn)行產(chǎn)生監(jiān)控器，監(jiān)控器分別根據(jù)（1）和（2）獲取的系統(tǒng)執(zhí)行軌跡和需求規(guī)約進(jìn)行重寫邏輯的運(yùn)行時(shí)驗(yàn)證，并顯示驗(yàn)證結(jié)果。

4.2工具實(shí)現(xiàn)

4.2.1插裝獲取系統(tǒng)執(zhí)行軌跡模塊實(shí)現(xiàn)

該模塊的作用是通過Spring AOP插裝獲取目標(biāo)系統(tǒng)的執(zhí)行軌跡。在該模塊中，GetSystem Trace類調(diào)用目標(biāo)系統(tǒng)運(yùn)行，RBC2RBCAspect類根據(jù)配置的插裝點(diǎn)進(jìn)行代碼插裝，當(dāng)目標(biāo)系統(tǒng)運(yùn)行完成后，RBC2RBCAspect類的通知代碼獲取系統(tǒng)的執(zhí)行軌跡序列。然后由GetSystem Trace類生成原子命題聲明文件與執(zhí)行軌跡序列日志文件。如圖5所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

圖5　插裝獲取系統(tǒng)執(zhí)行軌跡模塊靜態(tài)結(jié)構(gòu)圖

4.2.2需求規(guī)約導(dǎo)入模塊實(shí)現(xiàn)

該模塊的作用是導(dǎo)入從LSC轉(zhuǎn)換所得的LTL公式，同時(shí)生成相應(yīng)的需求規(guī)約文件并將其存儲在本地，生成的需求規(guī)約文件將作為需求規(guī)約輸入到Maude工具引擎中。如圖6所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

圖6　需求規(guī)約導(dǎo)入模塊靜態(tài)結(jié)構(gòu)圖

4.2.3運(yùn)行時(shí)驗(yàn)證模塊實(shí)現(xiàn)

該模塊的作用是調(diào)用Maude工具引擎進(jìn)行運(yùn)行時(shí)驗(yàn)證。該模塊中，RunDemo類生成相應(yīng)的重寫規(guī)則，Maude工具引擎根據(jù)重寫規(guī)則文件進(jìn)行運(yùn)行時(shí)驗(yàn)證，并顯示運(yùn)行時(shí)驗(yàn)證結(jié)果。如圖7所示是本模塊的靜態(tài)結(jié)構(gòu)圖。

圖7　運(yùn)行時(shí)驗(yàn)證模塊的靜態(tài)結(jié)構(gòu)圖

4.2.4驗(yàn)證過程

第一，插裝獲取系統(tǒng)執(zhí)行軌跡。首先，工具將導(dǎo)入并運(yùn)行目標(biāo)系統(tǒng)，當(dāng)目標(biāo)系統(tǒng)運(yùn)行結(jié)束后，工具就獲取了執(zhí)行軌跡序列。第二，導(dǎo)入待驗(yàn)證的需求規(guī)約，輸入從LSC轉(zhuǎn)換所得的LTL公式形式的需求規(guī)約。最后，進(jìn)行運(yùn)行時(shí)驗(yàn)證。工具首先生成重寫規(guī)則文件，然后調(diào)用Maude工具引擎，Maude工具引擎根據(jù)重寫規(guī)則產(chǎn)生預(yù)測監(jiān)控器，進(jìn)行運(yùn)行時(shí)驗(yàn)證，并顯示驗(yàn)證結(jié)果。本次實(shí)驗(yàn)結(jié)果如圖8所示。

本次實(shí)驗(yàn)結(jié)果為“maybe”，由于從LSC轉(zhuǎn)換所得的LTL公式含有時(shí)序邏輯運(yùn)算符G，驗(yàn)證工具分析目前的執(zhí)行軌跡沒有發(fā)生需求違約，但對以后的執(zhí)行情況還無法確定，判定結(jié)果為可能為真，因此驗(yàn)證結(jié)果為maybe，這也體現(xiàn)出LTL三值語義實(shí)現(xiàn)了對LTL二值語義的自然覆蓋。然后進(jìn)行另一組實(shí)驗(yàn)，本次插裝獲取另一條軌跡t=HOVCond，pre，req，ack，rri，使用工具進(jìn)行運(yùn)行時(shí)驗(yàn)證，該執(zhí)行軌跡的實(shí)驗(yàn)結(jié)果為“false”，如圖9所示。

圖8　運(yùn)行時(shí)驗(yàn)證

圖9　執(zhí)行軌跡違反規(guī)約的驗(yàn)證結(jié)果

5　結(jié)語

基于LSC的形式化驗(yàn)證方法已成為軟件開發(fā)過程中一種重要的驗(yàn)證方法，基于LSC的形式化驗(yàn)證已經(jīng)成功應(yīng)用到多個(gè)領(lǐng)域。本文對基于LSC的形式化驗(yàn)證方法進(jìn)行研究，論述LSC的理論基礎(chǔ)，對比分析了基于LSC的形式化驗(yàn)證領(lǐng)域的關(guān)鍵技術(shù)與應(yīng)用進(jìn)展，并實(shí)現(xiàn)一種基于活性順序圖的驗(yàn)證工具，實(shí)驗(yàn)證明使用本驗(yàn)證工具進(jìn)行運(yùn)行時(shí)驗(yàn)證的可行性。隨著軟件規(guī)模不斷擴(kuò)大系統(tǒng)集成度不斷提高，基于LSC的形式化驗(yàn)證方法必將在軟件開發(fā)過程中發(fā)揮其應(yīng)有的價(jià)值。

［1］Li X S，Liu Z M，He J F.A formal semantics of UML sequence diagram［A］.Proceedings of the 2004 Australian Software Engineering Conference［C］.2004：168-177.

［2］Clarke E M，Grumberg O，Peled D A.Model Checking［M］.MIT press，1999.

［3］Leucker M，Schallhart C.A brief account of runtime verification［J］.The Journal of Logic and Algebraic Programming，2009，78（5）：293-303.

［4］ITU-T.Recommendation Z.120：Message Sequence Charts［Z］. Geneva：ITU-T，1999.

［5］Object Management Group （OMG）.UML［Z］：Superstructure Version 2.2.2009.

［6］Damm W，Harel D.LSCs：Breathing Life into Message Sequence Charts［J］.Formal Methods in System Design，2001，19（1）：45-80.

［7］李雯睿，王志堅(jiān)，張鵬程.模態(tài)順序圖u MSD的形式化語義［J］.軟件學(xué)報(bào)，2011，22（4）：659-675.

［8］Larsen KG，Li S.Scenario-based analysis and synthesis of real-time systems using Uppaal［A］.Proc13th Conference on Design，Automation，and Test in Europe［C］.2010：447-452.

［9］Harel D，Maoz S，Segall I.Some Results on the Expressive Power and Complexity of LSCs［J］.In Pillars of computer science，2008，351-366.

［10］Bontemps Y，Schobbens P.The Complexity of Live Sequence Charts［J］.Institut d'Informatique，University of Namurrue Grandgagnage，21B5000-Namur（Belgium），2005，15.

［11］Harel D，Segall I.Synthesis from scenario-based specifications［J］.Journal of Computer and System Sciences，2012：78（3），970-980.

［12］Harel D，Kantor A，Maoz S.On the Power of Play-Out for Scenario-Based Programs.［J］.Lecture Notes in Computer Science，2010：207-220.

［13］Brenner C，Greenyer J，Panzica V et al.The ScenarioTools Play-Out of Modal Sequence Diagram Specifications with Environment Assumptions［A］.In Proc.12th Int Workshop on Graph Transformation and Visual Modeling Techniques.Volume 58，EASST ［C］.2013.

［14］Bontemps Y，Schobbens P.The Computational Complexity of Scenario-based Agent Verification and Design［J］.Journal of Applied Logic，2007，5（2）：252-276.

［15］Kugler H，Harel D，Pnueli A et al.Temporal logic for scenariobased specifications［A］.Proc.of the 11th Int.Conf.on Tools and Algorithms for the Construction and Analysis of Systems（TACAS05）［C］.2005：3440，445-460.

［16］Kumar R，Mercer E，Bunker A.Improving translation of live sequence charts to temporal logic［A］.Proc.of the 7th Int.Conf. on Automated Verification of Critical Systems（AVoCS07）［C］. 2007，183-197.

［17］Kumar R，Eric G Mercer.Verifying Communication Protocols U-sing Live Sequence Chart Specifications［J］.Electronic Notes in Theoretical Computer Science，2009，250（2）：33-48.

［18］Kumar R，Mercer EG.Improved live sequence chart to automata translation for verification［J］.Electronic Communications of the EASST，Volume 10，2008.

［19］Li SH，Balaguer S，David A，G.Larsen K，Nielsen B，Pusinskas S.Scenario-based verification of real-time systems using UPPAAL［C］.Form Methods System Design，2010，37：200-264.

［20］張碩，賀飛.運(yùn)行時(shí)驗(yàn)證技術(shù)的研究進(jìn)展［J］.計(jì)算機(jī)科學(xué)，2014，41（11A）：359-363.

［21］Chai M，Schlingloff B.Monitoring Systems with Extended Live Sequence Charts［J］.Springer International Publishing Switzerland，RV 2014，LNCS 8734，48-63.

［22］Clavel，Duran，Marti-Oliet，Meseguer，Talcott et al.Maude Manual［M］ （version 2.6）.University of Illinois，Urbana-Champaign，2011.

Research on Formal Verification Method and Verification Tool Based on Live Sequence Chart

Zhang Kun，Ye Junmin，Wang Qiang，Zhao Lixian，Chen Shu
（School of Computer Science，Central China Normal University，Wuhan430079，China）

In recent years，the role of formal verification technology in the software development process is growing more and more important.How to use formal verification technology to improve the reliability of software systems is a major concerned problem of software developers and users.This paper summarizes the progress of formal verification method based on Live Sequence Chart recently.In this paper，the language of live sequence chart，its expressive power and complexity are first introduced.Then the existing key technologies and their application of formal verification method based on live sequence chart are analyzed.Finally，the runtime verification tool based on live sequence chart is implemented，experiments show the feasibility of using this verification tool to formal verification.

live sequence chart；formal verification；software development process

1671-4598（2016）05-0274-05

10.16526/j.cnki.11-4762/tp.2016.05.076

TP393

A

2015-11-14；

2015-12-15。

國家科技支撐計(jì)劃項(xiàng)目（2015BAK33B00）；教育部規(guī)劃基金項(xiàng)目（15YJA880095）；中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金科研項(xiàng)目（CCNU15GF003）。

張坤（1992-），湖北武漢人，碩士研究生，主要從事軟件分析與驗(yàn)證方向的研究。