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

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

（華中師范大學　　計算機學院，武漢　430079）

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

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

（華中師范大學計算機學院，武漢430079）

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

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

0　引言

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

基于場景的形式化驗證經(jīng)常使用順序圖對系統(tǒng)進行建模和分析，順序圖是一種基于場景的語言，能夠圖形化地表示系統(tǒng)實例間交互的時序關(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表達能力很有限，只能表示可能發(fā)生的場景，不能表示系統(tǒng)必須滿足的場景。雖然UML-SD增加了一些新的操作符，增強了其表達能力，但UML-SD的非形式化語義也限制了其應(yīng)用。LSC對MSC進行擴展，LSC使用universal和existential兩種模式區(qū)分強制場景和可能場景，且LSC具有形式化語義。因此，軟件開發(fā)過程中形式化驗證經(jīng)常使用LSC描述系統(tǒng)場景中事件交互的時態(tài)關(guān)系。此外，LSC可以用來建模實際系統(tǒng)，也可以用于描述場景需求，基于LSC的形式化驗證方法不僅使系統(tǒng)需求的行為語義易于理解，而且還能盡早地發(fā)現(xiàn)軟件設(shè)計錯誤。利用LSC對系統(tǒng)進行建模和分析已成為需求分析階段的重要技術(shù)和方法。

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

圖1　universal模式LSC圖

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

1　LSC語言定義

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

1.1LSC語法

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

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

1）I是實例線的結(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基于軌跡的語義時要使用LSC的cut，這里首先定義LSC的cut。

定義2（cut［8］）一個cut指圖中每個實例到其位置的一個映射，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中事件的集合。

一個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語言的表達能力與復雜性論述

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

2　基于LSC的形式化驗證方法

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

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

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

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

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

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

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

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

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

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

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

2.2.2LSC轉(zhuǎn)換為自動機

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

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

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

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

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

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

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

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

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

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

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

3.2基于LSC形式化方法的運行時驗證

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

圖3　基于LSC形式化方法的運行時驗證過程

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

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

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

4.1工具架構(gòu)

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

圖4　運行時驗證工具框架

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

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

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

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

3）運行時驗證：

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

4.2工具實現(xiàn)

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

該模塊的作用是通過Spring AOP插裝獲取目標系統(tǒng)的執(zhí)行軌跡。在該模塊中，GetSystem Trace類調(diào)用目標系統(tǒng)運行，RBC2RBCAspect類根據(jù)配置的插裝點進行代碼插裝，當目標系統(tǒng)運行完成后，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ī)約導入模塊實現(xiàn)

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

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

4.2.3運行時驗證模塊實現(xiàn)

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

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

4.2.4驗證過程

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

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

圖8　運行時驗證

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

5　結(jié)語

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

［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］李雯睿，王志堅，張鵬程.模態(tài)順序圖u MSD的形式化語義［J］.軟件學報，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］張碩，賀飛.運行時驗證技術(shù)的研究進展［J］.計算機科學，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。

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

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