基于有窮論域下區(qū)間時序邏輯的模型檢測研究?

李 超

（西安郵電大學計算機學院 西安 710061）

1 引言

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

2 概念

2.1 模型檢測

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

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

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

2.2 區(qū)間時序邏輯

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

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

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

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

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

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

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

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

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

2.3 自動機

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

3 模型檢測關鍵技術研究

3.1 模型檢測流程

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

圖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）。

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

算法 1 function cfa（p）

/*前置條件：P為經過預處理過的ITL公式*/

/*后置條件：cfa（P）為公式 P構造的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)都是程序各變量的一種賦值。

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

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

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

ransistions：：= ｛edge｝

edge ：：=（s1，cond，s2）

自動機數據格式中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)層次架構

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

圖3 系統(tǒng)架構

4.2 用戶交互界面

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

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

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

圖4 界面

4.4 基礎服務層

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

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

5 結語

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