基于多引擎并行協作的SCADE模型檢測

方雨瑤,張 聰

(南京航空航天大學 計算機科學與技術學院,江蘇 南京 211106)

0 引 言

隨著科技的發展,反應式系統[1]在航空航天、交通、核工業等關鍵性領域應用越來越廣泛,它能夠以確定的時間對其所處的環境做出連續反應,具有時間約束性、可預測性、與外部環境的交互性等。為了方便反應式系統的設計與實現,領域專家與學者提出了同步語言[2]。其中SCADE(Safety Critical Application Development Environment)語言[3-5]是這些領域的事實標準開發語言,已經被廣泛應用于實現實時嵌入式自動控制系統[6]。這些領域對系統的安全性與可靠性要求非常高,因此這些系統需要經過嚴格的形式化驗證[7]。

現有的SCADE Suite工具可以對SCADE程序進行模型檢測,但該工具是一款價格昂貴的商業軟件,且已經限制在國內使用和研究,并且驗證方法單一、驗證效率不高[8-9]。而由Henning Basold等人開發的免費工具不支持完整的SCADE語言,并且驗證效率較低[10]。

基于現狀,該文提出了基于多引擎并行協作的SCADE模型檢測方法。將SCADE程序和待驗證的安全屬性轉化為一階邏輯公式,并對一階邏輯公式使用SMT(Satisfiability Modulo Theories)求解器,通過多引擎并行協作的方法進行驗證。主要工作如下:

(1)提出并行執行BMC(Bounded Model Checking)引擎、歸納法引擎,將原本k-Induction算法中串行的基礎步驟和歸納步驟改為并行執行。

(2)提出程序抽象引擎,對大型復雜程序進行抽象,并反復進行檢測、確認、精化,加快對無效屬性的驗證速度。

(3)開發了一款SCADE模型檢測工具PSMC,實現BMC引擎、歸納法引擎和程序抽象引擎并行協作的驗證架構,經過實驗證明了相比于不使用優化時能夠提高驗證效率,從而可以對較大規模的程序進行驗證。

1 相關工作

傳統的k-Induction算法[11]以1-Induction標準歸納法為基礎,當標準歸納法無法證明“性質在系統執行的第i步成立”蘊含“性質在系統執行的第i+1步成立”時,對待驗證公式進行擴展,嘗試證明“性質在系統執行的第n+1到n+k步內成立”蘊含“性質在系統執行的第n+k+1步成立”。假設一個有限狀態遷移系統S=,其中X是系統所有狀態變量的集合,xi表示系統所有狀態變量在時鐘i下的瞬時值,I表示系統的初始狀態,T是系統在前一個時鐘到當前時鐘的遷移關系表達式。要驗證屬性P是有效的,即證明P在有限遷移系統S中是不變式(在有限遷移系統S的所有可達狀態都滿足P)。k-Induction算法所依賴的驗證公式包括公式(1)和公式(2)。如果它們在某個時刻k(k≥0)都成立,即可證明P是不變式。

T(0)∧…∧T(k)?P(0)∧…∧P(k)

(1)

T(n)∧…∧T(n+k+1)∧P(n)∧…∧P(n+k)?P(n+k+1)

(2)

傳統的k-Induction算法中基礎步驟公式(1)和遞歸步驟公式(2)是串行協作的關系,也就是說,公式(2)的檢查需要依賴于公式(1)的檢查結果。由此帶來的一個后果是,當屬性無效且在k值較大才能被證偽的情況下,串行驗證會消耗大量時間在遞歸步驟公式(2)的驗證上。為了提高驗證效率,將串行協作優化為并行協作,將基礎步驟作為單獨線程,將遞歸步驟也作為單獨線程,再通過消息傳遞機制控制線程之間的關系,這樣算法引擎就可以在各自的線程上并行地同時運行,可以使得有效屬性和無效屬性的驗證速度大大加快。接下來,詳細描述多引擎并行協作算法的實現。

2 多引擎并行協作方法

圖1展示了多引擎并行協作的架構設計。首先,詞法語法解析器將SCADE同步語言程序解析為抽象語法樹[12](AST),然后邏輯公式生成器將AST轉化為求解器可求解的邏輯公式,最后BMC引擎、歸納法引擎和程序抽象引擎分別調用獨立的SMT求解器(例如Z3)[13]同時對邏輯公式進行求解,得到驗證結果。注意,在求解階段設定了一個固定的k值,在k_opt步之前由BMC引擎和歸納法引擎并行執行,在k_opt步之后由程序抽象引擎和歸納法引擎并行執行,并且通過共享變量進行消息傳遞和協作。

圖1 PSMC的架構設計

2.1 BMC引擎

BMC引擎從k=0開始驗證公式(1),并逐漸遞增k的值,如果在某個k值下公式不成立,求解器會返回一組可以證明公式不成立的變量值,稱之為反例。再將無效屬性和反例輸出后終止該線程,同時將終止線程信號M1=Abort傳遞給歸納法引擎所處的線程。否則,將繼續遞增k值,并將成功通過該公式驗證的k值通過信號M1=k傳遞給歸納法引擎線程,直到接收到由歸納法引擎所處線程傳遞來的終止線程信號M2=Abort,終止本線程。

2.2 歸納法引擎

線程休眠,直到接收到來自BMC引擎線程或程序抽象引擎線程消息M1。如果M1=Abort是終止線程信號,也就是說,BMC引擎或程序抽象引擎已經證明了屬性是不成立的,則終止本線程。如果M1=k是自然數,也就是說,BMC引擎或程序抽象引擎發現屬性在第k個時鐘以內是成立的,則對于所有的自然數i≤k,調用SMT求解器驗證歸納公式(2)是否成立。如果對于某個i歸納公式(2)成立,那么對于所有的時鐘c(c>0),基礎公式(1)都是成立的,即證明了屬性是成立的。此時輸出有效屬性,并將終止線程信號M2=Abort傳遞給BMC引擎線程和程序抽象引擎線程,然后終止本線程。如果歸納公式(2)不成立,歸納法引擎則繼續遞增k值對公式(2)進行驗證,直到k值遞增到大于M1傳遞來的自然數,歸納法引擎繼續休眠直到再次接收到來自BMC引擎線程或程序抽象引擎線程消息M1。

2.3 程序抽象引擎

在多引擎并行協作的架構上設定一個控制BMC引擎和程序抽象引擎的臨界值k_opt,當BMC引擎的變量kk_opt時,BMC引擎所處線程進入休眠狀態并且啟動程序抽象引擎,對程序進行抽象后,進行BMC檢測,如果沒有報告反例,說明該抽象程序在k個時鐘以內滿足待驗證屬性,則通過信號M1=k將通過檢查的k值傳遞給歸納法引擎;如果報告了反例,且經過確認該反例確實為真實反例,可以得出該屬性無效的結論,則輸出反例所違反的屬性(即無效屬性)和反例,并將終止線程信號M1=Abort傳遞給歸納法引擎所處線程,然后終止本線程。如果接收到歸納法引擎所處線程傳遞來的終止線程信號M2=Abort,則終止本線程。否則,k值加1繼續進行抽象程序算法檢測。

圖2是程序抽象引擎采用的程序抽象算法流程。首先,對目標程序進行初始化抽象,將抽象程序進行BMC算法檢測,如果檢測過程中出現反例,那需要對該反例進行確認,判斷該反例是否為偽反例,如果是,那么需要對抽象程序進行精化操作使抽象程序更靠近原程序;如果不是,則得出該屬性無效的結論。接下來將對反例引導的抽象精化算法進行詳細的說明。

圖2 程序抽象算法流程

如圖2,首先將對邏輯公式轉化器處理完的程序N進行抽象處理,得到初始抽象程序N'。原程序四元組N中有輸入數據流I,局部數據流L,輸出數據流O。用set集合存儲了程序的等式依賴關系,通過等式依賴關系集合,得到待驗證屬性P依賴與ya、yb,注意,這里提到的依賴為等式等號左側和右側直接的關系,比如有a=b+c,就有>,a依賴于b和c的值;接下來將闡述構建抽象程序的過程。原始程序N記為四元組N=,其中的輸入數據流I、局部數據流L、輸出數據流O都作為抽象程序N'的輸入數據流I',將輸出數據流O'置為空集,將待驗證屬性和其依賴的變量作為抽象程序N'的局部數據流L',將P的等式定義eqp,以及P所依賴變量ya、yb的等式定義eqya、eqyb作為新的等式集合E'。按照這樣的規則構建了新的抽象程序四元組N=。

在對原程序進行初始抽象后,對抽象程序進行BMC算法檢測,如果檢測出反例,需要判斷該反例是真實的還是虛假的。SMT求解器返回的反例由步數k,變量以及變量對應的值構成,將源程序同樣提取一階邏輯公式,去檢測反例所顯示的變量狀態是否是源程序可達的變量狀態,也就是說,用SMT求解器去檢測反例是否是由源程序在k步下可達的狀態,如果求解器返回unsat證明反例表示的狀態不可達,該反例是偽反例,同時可以從求解器中獲得unsatcore(unsatcore為使得檢測的式子不滿足的關鍵變量的集合),再根據獲得的unsatcore對抽象程序進行抽象精化;如果求解器返回sat證明反例表示的狀態可達,該反例是真實反例,得出該檢測屬性無效,停止檢測。

算法1:refine算法

Inputs:unsatcore , map m:V→2V

priorty_queue Q;

foreach var in unsatcore

Q.push(var);

while(Q.size>0)

node = Q.pop();

if ( is_undefined(node) )

refine_var(node);

else if ( is_fully_refined(node) )

continue;

else

dependencies dep_set = map.get(node);

foreach temp_var in dep_set

Q.push(temp_var);

經過反例確認后,如果該反例是偽反例,那需要根據獲得的unsatcore對抽象程序進行精化操作,具體的過程在算法1中展示。將所有的變量用refined,undefined,ori-input標記;標記為refined或undefined的變量對應源程序中的非輸入變量,標記為ori-input的變量對應源程序的輸入變量;refined標記的變量指該變量在抽象程序中已得到等式定義的約束,也就是說該變量的等式定義已在抽象程序的等式集合中定義;undefined標記的變量指的是還未得到等式定義約束的變量;其中,如果某一變量和它的依賴變量都得到了等式定義的約束,那稱這個變量是fully-refined。

3 實驗分析

在Linux環境下使用C++語言開發實現了一款SCADE同步語言程序模型檢測工具PSMC(Parallel Scade Model Checker),該工具實現了多引擎并行協作模式和程序抽象引擎。在實驗過程中,首先采用未進行優化的串行驗證工具,之后再開啟PSMC的BMC引擎和歸納法引擎對比串行驗證和并行協作的驗證效率,再開啟程序抽象引擎,觀察程序抽象引擎對PSMC工具帶來的效率提升,以證明多引擎并行協作可以有效提升SCADE同步語言程序驗證的效率。

筆者構建了包含887個SCADE同步語言程序(分為七個文件夾)的測試集,該測試集是根據 Lustre標準測試集[14]、利用SCADE Suite工具[15]人工手動建模而來,與Lustre標準測試集的功能等價。將測試集按照最終的驗證結果劃分為三種,無效屬性(invalid)測試集、有效屬性(valid)測試集、驗證超時(timeout)測試集。其中無效屬性測試集中有359個無效屬性,有效屬性測試集中有305個無效屬性,設置了一個運行時間限制(100 秒),導致還有一種驗證結果為超時,所以測試集中有包含223個超時屬性的測試集。

表1展示了針對無效屬性測試集逐個增加優化算法的驗證時間對比,Size指的是測試集的大小,也就是無效屬性的數量,Depth指的是測試集中檢測出無效屬性產生反例時k的最大值,統計的運行時間是一個測試集的時間總和。表2展示了針對有效屬性測試集逐個增加優化算法的驗證時間對比,Size表示測試集中有效屬性的數量,Depth表示測試集中有效屬性被證明成立時k的最大值。兩個表格中的M1指的是加入了BMC引擎和歸納法引擎雙引擎并行協作的方法,M2指在M1的基礎上加入程序抽象引擎。

表1 無效測試集運行時間對比

從表1可見在無效屬性測試集中,表格中雙引擎并行協作能提速6%左右,抽象程序引擎的加入能在之前的基礎上提速26%左右,四種優化算法一共能提速31%左右,PSMC的整體運行速度明顯快于優化前,在Depth較大的測試集中PSMC的提速更加明顯。其中functionalchain測試集中驗證結果為無效的屬性個數為0。

表2 有效測試集運行時間對比

從表2可見在有效屬性測試集中,多引擎并行協作的效果在大部分測試集上耗時區別不大,甚至并行協作架構的加入使得部分測試集驗證時間變長了,經過分析實驗結果和實驗代碼,發現有效性大多都在k遞增到一步或者兩步時被檢出,其耗時在微秒級別。而多引擎并行協作時,線程之間的交互以及線程協作過程中線程的等待也會消耗一定的時間,但單個程序微妙級別耗時的增加在實際工具使用中不會帶來特別大的影響,實際操作中更注重工具在復雜問題上帶來的顯著提速效果,通過后續優化算法的加入可以盡量抵消這部分時間的消耗。

4 結束語

由于當前模型檢測工具對SCADE程序驗證的支持存在不足,該文提出了一種基于多引擎并行協作的SCADE程序模型檢測方法,并開發了PSMC。實驗表明,該方法不僅能夠很好地對SCADE同步語言程序進行自動、直接地驗證,而且相比于未使用優化時能明顯提高驗證效率。在未來的工作中,會在多引擎并行協作架構的基礎上加入更多先進的算法引擎,進一步提高SCADE同步語言程序的驗證效率,并在這一背景下驗證這些算法的效率。