李 超

（西安郵電大學(xué)計算機學(xué)院 西安 710061）

1 引言

模型檢測［1～2］是形式化驗證的一種重要方法，它以自動化的驗證技術(shù)克服了演繹證明的局限性得到了人們的青睞。區(qū)間時序邏輯（Interval Tem?poral Logic，ITL）是線性時序邏輯的一個重要分支，在模型檢測中有很大的利用價值。模型檢測可以幫助人們自動地驗證系統(tǒng)屬性的正確性，從而從根本上減少了系統(tǒng)的錯誤，降低了系統(tǒng)維護的成本。模型檢測是建立在邏輯的可判定性的基礎(chǔ)上，文獻［3］已經(jīng)證明了有窮論域下區(qū)間時序邏輯的可判定性，但是目前基于區(qū)間時序邏輯的模型檢測工具寥寥無幾，而現(xiàn)有的區(qū)間時序邏輯的模型檢測工具在建模和性質(zhì)描述上都有很大的不便利性，給用戶的使用帶來了極大的不便。本文在有窮論域下區(qū)間時序邏輯的判定性的基礎(chǔ)上利用自動機技術(shù)給出了一個模型檢測工具的設(shè)計及實現(xiàn)。

2 概念

2.1 模型檢測

在計算機科學(xué)中，模型檢測指的是給定一個系統(tǒng)模型，徹底地、自動地檢查該模型是否符合某個給定的要求。一般的，在軟件或者硬件系統(tǒng)中，給定的要求一般包含像無死鎖的這樣的安全需求和一些可能導(dǎo)致系統(tǒng)崩潰的關(guān)鍵狀態(tài)。模型檢測是一種自動化地驗證有窮狀態(tài)系統(tǒng)的屬性正確性的技術(shù)。

為了利用算法解決模型檢測的問題，系統(tǒng)模型和要求說明都必須用精確的數(shù)學(xué)語言來表達。為達到這樣的目的，模型檢測被表述為一個邏輯運算過程，也就是檢驗一個給定的系統(tǒng)模型是否滿足某個邏輯公式。一個簡單的模型檢測例子是驗證一個系統(tǒng)是否滿足一個由邏輯公式描述的性質(zhì)。如圖1所示。

圖1 模型檢測系統(tǒng)

2.2 區(qū)間時序邏輯

時序邏輯（Temporal Logic，TL）［4～5］的思想是：在一個模型中，公式的真與假不是靜態(tài)的，在一個包含多個狀態(tài)的模型中一個公式可以在某些狀態(tài)下滿足且在其他狀態(tài)下不滿足。時序邏輯在形式化驗證中已經(jīng)有了重要的應(yīng)用，即它被用來表達硬件和軟件系統(tǒng)的要求。比如，我們可能有這樣的要求“不管什么時候做出請求，對資源的獲取最終會被準(zhǔn)許，但是不會同時允許兩個請求者同時獲得資源”，這樣的一個描述可以很方便地用時序邏輯表達。

區(qū)間時序邏輯（Interval Temporal Logic，ITL）［6～7］同樣是一種線性時序邏輯，它可以表達在時間區(qū)間上的命題邏輯和一階邏輯，它有能力表達順序和并行的組合情況。區(qū)間時序邏輯處理的是有窮的狀態(tài)序列而不是無窮的序列。區(qū)間時序邏輯在計算機科學(xué)、人工智能、語言學(xué)領(lǐng)域中都得到應(yīng)用。

定義1 區(qū)間時序邏輯的項e和公式P的定義由下面BNF給出：

其中，d∈D為常量，D為任何數(shù)據(jù)類型的有窮論域；a∈V是靜態(tài)變量；x∈V是動態(tài)變量；v∈V是任意的靜態(tài)變量或者動態(tài)變量，其中V為靜態(tài)變量和動態(tài)變量的可數(shù)集合；p∈Prop為原子命題，其中Prop是原子命題的可數(shù)集合；f(e1，…，em)與 ρ(e1，…，em)分別表示 D上帶有m元參數(shù)的函數(shù)與謂詞；(N ext)，+(C hop Plus)是原始時態(tài)操作符。

在ITL的語法定義中，常量d、函數(shù) f及謂詞ρ均與其所在論域D是相關(guān)的。例如true和false是布爾論域B中的兩個常量；0，1，2，…是非負整數(shù)集合 N0（N0為非負整數(shù)集合）上的常量，+，-，×，∕是 N0上的函數(shù)，且 ＜，≤，＞，≥ 是 N0上的謂詞。

定義3 （基本ITL公式）基本ITL（Basic ITL，BITL）公式是滿足下列三個條件的公式：

1）公式中不包含任何時態(tài)項；

2）公式中所有等詞均形如v=d，其中v∈V為變量，d∈D為常量；

3）公式中不包含任何除等詞（=）之外的其他原始謂詞。

2.3 自動機

自動機［7］理論已經(jīng)在很多領(lǐng)域有廣泛的應(yīng)用，同時它在模型檢測中也起著至關(guān)重要的作用。有窮自動機可以被看作是一個帶有有窮輸入的設(shè)備，而它可以接受或者拒絕這個輸入。這個設(shè)備會隨著它從左到右讀取輸入而變化自己的狀態(tài)。在有窮自動機處理完成一個輸入后可以得到的僅是最終它到達的狀態(tài)的種類，也就是接受或者不接受。有窮自動機只接受有窮行為的特性不能滿足一些系統(tǒng)的需求。Büchi自動機［9～10］將有窮自動機擴展到可以接受無窮輸入，當(dāng)Büchi自動機的一次執(zhí)行無限到達某個終結(jié)狀態(tài)，那么它就接受一個無窮輸入。Büchi自動機是瑞士數(shù)學(xué)家Julius Richard Büchi在1962年發(fā)明的。目前Büchi自動機已經(jīng)成功應(yīng)用到基于 LTL［11～12］的模型檢測工具 SPIN［13～14］中，但由于Büchi自動機本身只能接受無窮行為，卻不能接受有窮行為，故在驗證時存在缺陷。完全有窮自動機（Complete Finite Automata，CFA）結(jié)合了有窮自動機和Muller自動機［15～16］的優(yōu)點，能夠接受有窮行為和無窮行為。

3 模型檢測關(guān)鍵技術(shù)研究

3.1 模型檢測流程

ITL模型檢測工具的工作流程圖如圖2所示，首先需要構(gòu)造出描述系統(tǒng)模型的系統(tǒng)自動機（Sys_CFA）和描述性質(zhì)的性質(zhì)自動機（P_CFA），然后對P_CFA進行自動機的求反運算得到性質(zhì)非自動機～P_CFA，最后對系統(tǒng)自動機和性質(zhì)非自動機求交判斷系統(tǒng)是否滿足性質(zhì)。

圖2 模型檢測流程圖

3.2 利用自動機進行模型檢測

定義4（完全有窮自動機）一個完全有窮自動 機 （CFA） 定 義 為 一 個 六 元 組A={ }

Σ，Q，δ，I，F(xiàn)，C ，其中：Σ 為字母表；Q 表示狀態(tài)集合；δ：Q×Σ→2Q是狀態(tài)遷移集合；I∈Q表示初始狀態(tài)集合；F?Q表示有窮可接受狀態(tài)集合；C?2Q表示無窮可接受條件集合。

特別的，如果|I|=1且δ為Q×Σ→Q，則稱 A是確定的完全有窮自動機（Deterministic Complete Finite Automata，DCFA），否則為非確定的完全有窮自動機（Nondescripteterministic Complete Finite Au?tomata，NCFA）。

模型檢測工具的性質(zhì)描述是使用ITL公式，而在把ITL公式轉(zhuǎn)換成自動機之前，需要將描述性質(zhì)的ITL公式化簡成基本ITL公式。此時整個公式就只包含原子命題，將CFA字母表中的字符定義為原子命題或其非的集合就可以構(gòu)造出對應(yīng)的自動機。對于化簡后的ITL公式的原子命題集合Prop，ITL公式的CFA字母表Σ定義為對于任意的非空集合Φ∈Prop，令為了方便起見，令{Δ}(Δ ∈Σs)表示 Σ 所有以 Δ 為子集的字符的集合，即{a |a∈Σ，Δ?a} ，特別的true表示集合 Σ 。相應(yīng)的，用遷移{q1，Δ，q2}(Δ ∈Σs)表示從狀態(tài)q1到q2存在多個遷移且全部遷移的標(biāo)記集合為{Δ}。對于遷移{q1，{t r ue}，q2}表示q1到q2存在的遷移標(biāo)記包含了Σ中所有字符。邏輯公式到CFA的構(gòu)造算法如算法1所示。

算法 1 function cfa（p）

/*前置條件：P為經(jīng)過預(yù)處理過的ITL公式*/

/*后置條件：cfa（P）為公式 P構(gòu)造的CFA A(P ) =(Σ ，Q，δ，I，F(xiàn)，C ) */

begin function

case

P為原子命題 p：

end case

returnA(P)；

end funcation

3.3 系統(tǒng)建模

要使用模型檢測工具對一個系統(tǒng)進行檢測必須首先對該系統(tǒng)進行建模。狀態(tài)是描述一個系統(tǒng)的核心概念。狀態(tài)表示了系統(tǒng)在執(zhí)行中的某個確定時刻的一些信息，一個狀態(tài)可以用程序的每個變元的一種賦值來表示，例如一個使用程序變量作為自由變元的一階公式可以表達一組滿足該公式的程序狀態(tài)集合，其中每個狀態(tài)都是程序各變量的一種賦值。

利用轉(zhuǎn)換系統(tǒng)建模通常是很方便的。轉(zhuǎn)換系統(tǒng)可以描述系統(tǒng)的行為，在轉(zhuǎn)換系統(tǒng)中，系統(tǒng)可以處于某一個狀態(tài)。一個轉(zhuǎn)換表示系統(tǒng)的一個操作，在每一個狀態(tài)上，系統(tǒng)可以執(zhí)行一系列轉(zhuǎn)換中的一個而到達其他狀態(tài)。

自動機本身就是一種狀態(tài)轉(zhuǎn)換系統(tǒng)，在建模時，系統(tǒng)的狀態(tài)和狀態(tài)之間轉(zhuǎn)換的條件是比較直觀的，轉(zhuǎn)換條件直接用邏輯公式給出，清晰地表達出了系統(tǒng)狀態(tài)之間的關(guān)聯(lián)。所以我們直接用自動機進行系統(tǒng)建模。為了建模方便我們定義了一種自動機數(shù)據(jù)格式用來表達自動機，這樣可以使用戶方便的建模，也方便轉(zhuǎn)換為自動機。自動機數(shù)據(jù)格式的定義如下。

Model：：= ｛propSet，constSet，varSet，stavarSet，sta?tusSet，initStatus，transitions，acceptables，infaccp｝

ransistions：：= ｛edge｝

edge ：：=（s1，cond，s2）

自動機數(shù)據(jù)格式中propSet是建模時所需的原子命題的集合；constSet是常量集合；varSet是動態(tài)變量集合；stavarSet是靜態(tài)變量集合；statusSet是系統(tǒng)的自動機模型的狀態(tài)集合；initStatus是自動機模型的初始狀態(tài)集合，它是statusSet的子集；transi?tions是自動機的遷移的集合，每個遷移又是邊edge；edge定義中s1和s2是屬于statusSet的狀態(tài)，cond是遷移上的條件；acceptables是自動機可接受條件的集合；infaccp是系統(tǒng)中可以一直循環(huán)下去的路徑的集合，即自動機無窮可接受條件的集合。

4 系統(tǒng)實現(xiàn)

4.1 系統(tǒng)層次架構(gòu)

整個系統(tǒng)分為三層，基礎(chǔ)服務(wù)層、核心功能層、交互界面層。如圖3所示。用戶交互層主要是用戶建模和輸入性質(zhì)公式的接口并呈現(xiàn)模型檢測的結(jié)果，核心功能層負責(zé)實現(xiàn)整個模型檢測的算法，基礎(chǔ)服務(wù)層為核心功能層提供一些通用的功能，例如集合的運算、圖的相關(guān)算法等。

圖3 系統(tǒng)架構(gòu)

4.2 用戶交互界面

用戶交互界面如圖4所示，圖中第一部分是用戶輸入性質(zhì)公式的區(qū)域，第二部分是用戶輸入系統(tǒng)模型的區(qū)域，第三部分是系統(tǒng)呈現(xiàn)模型檢測結(jié)果的區(qū)域，第四部分是驗證開始的按鈕。

4.3 核心功能實現(xiàn)

系統(tǒng)的核心功能主要包括兩大部分，分別是將性質(zhì)公式和系統(tǒng)模型轉(zhuǎn)換成自動機再進行運算。在轉(zhuǎn)換過程中用到的主要功能有詞法分析、語法解析樹構(gòu)造、自動機的構(gòu)造以及運算，而自動機的運算包括遷移條件之間的運算和字母之間的運算，還包括子集構(gòu)造法和預(yù)處理這些重點功能。

圖4 界面

4.4 基礎(chǔ)服務(wù)層

基礎(chǔ)服務(wù)層主要為核心功能層服務(wù)。由于系統(tǒng)使用的主要技術(shù)是自動機，在系統(tǒng)中自動機是以類似于圖的形式保存的，所以有大量關(guān)于圖的運算功能比如圖的遍歷等，我們將圖的這些算法放在基礎(chǔ)層增加了代碼的重用性。

系統(tǒng)中的邏輯公式或遷移條件是以集合形式保存的，自動機的運算本質(zhì)上是邊上遷移條件的運算，所以集合的運算功能放在基礎(chǔ)服務(wù)層。

5 結(jié)語

本文通過結(jié)合自動機技術(shù)實現(xiàn)了有窮論域下區(qū)間時序邏輯的判定算法，解決了一階邏輯判定時變量與函數(shù)的處理問題，給出了從區(qū)間時序邏輯公式到完全有窮自動機的構(gòu)造算法，并提出了基于自動機的模型檢測工具的建模方法。最后給出了有窮論域下區(qū)間時序邏輯模型檢測工具的實現(xiàn)方法。