ＰＲＯＭＥＬＡ語義引擎執行研究

摘要：模型檢查工具SPIN的核心是PROMELA語言，對PROMELA語言執行方式的理解決定所描述系統模型的行為方式。該文從語義角度研究了 PROMELA語義引擎問題。首先給出PROMELA語法的抽象對象模型形式化定義，然后給出一個算法來實現PROMELA語法到抽象對象模型的映射，描述 了PROMELA指稱語義。

關鍵詞：模型檢查；SPIN；PROMELA；語義

中圖分類號：TP315文獻標識碼：A文章編號：1009-3044(2008)35-2159-02

Research on execution patterns of SPIN Semantics Engine

FENG Yan-qing

(School of Information and Technology， Jiangxi University of Finance and Economics， Nanchang 330013， China)

Abstract: The PROMELA language， whose commitment manners decide system executions， plays crucial role in model checking toolSPIN. This paper studies semantic engines of PROMELA. Firstly， a formal model of PROMELA is given. Secondly， the denotational semantics of PROMELA are described by the mapping between syntax of PROMELA and the model. We discuss the specific issuessuch as atomic sequence， rendezvous channel， and their solutions. Finally a case study demonstrates PROMELA workingprinciple.

Key words: model checking; SPIN; PROMELA; semantics

1 引言

模型檢查[1-2]在軟件開發中扮演非常重要的作用，模型檢查的基本思想是使用標記遷移系統（LTS）結構Μ=(S，R，L)描述軟件規格模型，使用時態邏輯描述軟件應具備的特性#981;，如活性、安全性和無死鎖等，然后使用一個算法檢查Μ，s|=#981;，如果成立表示系統具備所描述特性。

SPIN[3]是功能強大、業界普遍使用的模型檢查工具，對SPIN語言PROMELA語義的研究有助于更好地描述系統行為。

本文的目的是給出PROMELA語言的語義解釋。文中第二部分首先給出與PROMELA語言元素對應模型對象的形式化定義，然后給出一個算法來實現PROMELA語句到該模型的映射。

2 PROMELA的語義引擎

PROMELA語義引擎[4]決定了PROMELA描述的模型如何被解釋和執行。PROMELA語法由變量Variable、消息Message、消息通道Message Channel、進程Procress等部分構成。我們先給出這些語法對應模型的形式化定義，然后給出一個算法來實現PROMELA語句到模型的映射。

2.1 PROMELA語義模型

定義1：Variable（變量）

Variable是一個五元組(name，scope，domain，inival，curval)。name為變量標識符；scope指定變量的作用范圍，有全局和局部范圍之分；domain表示變量的值域；inival表示變量的初始值；curval表示變量的當前值。Variable的作用范圍可以是全局的或是局部的。對于特定的進程來說，變量的類型通常決定變量的值域。

定義2：Message (消息)

Message是Variable（變量）的一個有序集合，表示進程間所交換的數據。

定義3：Message Channel（消息通道）

Message Channel是一個三元組(ch_id，nslots，contents)；ch_id是通道標識符；nslots表示消息通道中最多可以存儲的消息數；contents是消息的一個有序集合。消息通道沒有定義作用范圍，一個消息通道作用范圍總是全局的。理論上每一個活動進程都可以通過ch_id進行存取。

定義4：Procress（進程）

Procress是一個六元組(pid，lvars，lstates，initial，curstate，trans)；pid是進程標識符；lvars表示進程的局部變量有限集；lstates表示進程的局部狀態有限集；initial表示進程的初始狀態；curstate表示進程的當前狀態；trans表示進程中所有遷移的有限集；進程處于初始化狀態時有curstate= initial，，對于局部變量有curval=inival。

定義5：Tramstion（遷移）

進程中的Tramstion是一個七元組(tr_id，source，target，cond，effect，prty，rv)；tr_id是遷移標識符；source和target分別表示遷移的源狀態和目標狀態；cond是關于全局系統狀態的一個布爾條件；effect函數作用于全局系統狀態，它可以修改全局系統狀態；prty表示遷移的優先級，PROMELA中遷移的優先級由unless結構定義； rv表示遷移是同步通信(Rendezvous Channel)的接收消息操作。

定義6： System State（全局系統狀態）

全局系統狀態是元組(gvars，procs，chans，exclusive，handshake，timeout，else，stutter)；gvars表示全局變量有限集；procs表示進程的有限集；chans表示消息通道的有限集；exclusive默認值為0， 當atomic序列中的遷移執行時，會置exclusive為p.pid；handshake標志當前系統狀態下有無同步通信發生；布爾變量timeout提供了從系統阻塞狀態跳離的方法，僅當所有活動進程中沒有可執行遷移時它為true，否則它一直為1；布爾變量else當且僅當當前進程局部狀態下進程中沒有可執行性遷移時為true；stutter是布爾值，用來確定stutter規則是否起作用；在初始系統狀態，所有的進程位于其初始狀態，所有的全局變量滿足curval=inival；所有的消息通道滿足contents={}，exclusive 和handshake為0，timeout、else和stutter初始值為1。

定義1到定義6給出了PROMELA語言中抽象對象的形式化定義，這些抽象對象的關系如圖1所示。

2.2 PROMELA語句到語義模型的映射算法

下面我們探討具體的算法。

第一步：我們考察在系統狀態為s時，如何形成關于s的所有狀態空間。令元組(p，t)表示對應于系統狀態s時p進程及p中的一條可執行遷移t；集合E為二元組(p，t)的集合，它表示在系統狀態s下的所有活動進程的所有可能遷移，即求得在系統狀態s下的所有可能遷移狀態。算法executable( State s)輸入給定系統狀態 和所有活動進程，輸出集合E。executable(s)算法如下所示。

1 executable(State s)

2 {new Set E//創建關于元組(p，t)的集合E

3new Set e//創建關于元組(p，t)的集合e，中間變量

4E = {}

5timeout = 1

6AllProcs:

7for each active process p

8 { if (exclusive == 0//表示當前系統沒有遷移處于atomic序列

9 orexclusive == p.pid) //檢查進程p中atomic序列中的語句正在執行

10 { for u from high to low // 依P中遷移t優先級從高到低進行

11 { e = {};else = 1

12 OneProc: for each transition t in p.trans

13 {if (t.source == p.curstate

14andt.prty == u

15andeval(t.cond) == true

16and(handshake == 0

17or handshake == t.rv) )

18{ add (p，t) to set e }

19}

20if (e != {})//進程P中當前優先級下有可執行遷移

21{ add all elements of e to E //將可執行遷移t加入到E中

22break //結束優先級檢查循環

23}

24else if (else == 1) //進程P中當前優先級下無可執行遷移

25 { else = true//置else為true

26 goto OneProc//重新對p中遷移進行可執行性檢查

27 }

28}

29}

30 }

31if (E == {} and exclusive != 0) //表示atomic序列中遷移已經執行完畢

32{ exclusive = 0//重置exclusive為0并重新檢查所有活動進程

33goto AllProcs

34}

35if (E == {} and timeout == 1) //系統中無可執行遷移，重新進行選擇

36{ timeout = true

37goto AllProcs//重新檢查所有活動進程

38}

39return E //返回關于系統狀態s的所有可能執行遷移(p，t)

40 }

進程p中atomic序列中的遷移執行時，算法置系統變量exclusive為p.pid。在算法executable(s)中atomic序列是如下處理的：算法首先測試系統變量exclusive的值（算法第8、9行）以確保atomic序列中的遷移執行不被中斷，然后再執行其它測試。當atomic序列中的所有遷移都執行完畢后，應重置系統變量exclusive并檢查所有活動進程（算法第32、33行）。

第二步：我們考察PROMELA語義引擎隨機挑選路徑對全局系統狀態s影響。只要集合E不空，我們在E中隨機選擇一個二元組(p，t)并執行元組中的可執行遷移t，于是全局系統狀態會遷移到新狀態s'，t所屬進程p的局部狀態也會發生遷移；當集合E為空，系統停止運行。特別的，對應于S=S0，系統處于初始狀態，所有的進程Pi(i≥0)也處于初始狀態。

3 結束語

本文描述了PROMELA語法元素對應的語義模型，并通過算法描述了PROMELA隨機交叉執行方式的工作原理。算法的關鍵是處理PROMELA中atomic序列和同步通信問題，即通過對PROMELA語義模型中的handshake處理，實現將同步通信的發送消息操作和接受消息操作看作一個完整的動作。通過對exclusive的處理，實現atomic序列的執行不會被其它語句隨機交叉。理解PROMELA語義引擎的工作原理，將有助于我們理解模型檢查工具SPIN是如何對分布式并發系統進行建模和驗證的。

參考文獻：

[1] Ben-ari M.Principles of the Spin Model Checker[M].London:Springer-Verlag，2008.

[2] Baier C，Katoen J.Principles of Model Checking[M].London，England:The MIT Press，2008.

[3] Holzmann，J G.Spin Model Checker:Primer and Reference Manual[M].Addison-Wesley Professional:2003.

[4] 黎升洪，繆淮扣.時態邏輯描述能力比較研究[J].計算機工程與應用，2006(22).