ESpin*：基于SPIN 的Eclipse模型檢測(cè)環(huán)境

呂 威，黃志球，陳 哲，闞雙龍，魏 歐

南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京210016

1 引言

隨著軟件在信息化社會(huì)中發(fā)揮的作用日益重要，人們對(duì)軟件的正確性、可靠性、安全性等可信性質(zhì)的要求也越來(lái)越高，關(guān)鍵系統(tǒng)中的軟件失效不僅會(huì)導(dǎo)致生命財(cái)產(chǎn)的重大損失，甚至?xí)?lái)嚴(yán)重的社會(huì)問(wèn)題。對(duì)于復(fù)雜的并發(fā)系統(tǒng)和實(shí)時(shí)系統(tǒng)，由于系統(tǒng)運(yùn)行本身存在著不確定性，傳統(tǒng)的測(cè)試技術(shù)并不能充分保證其安全性，這時(shí)基于數(shù)學(xué)公式的形式化驗(yàn)證方法[1]就成為解決此類(lèi)問(wèn)題的重要途徑。模型檢測(cè)（Model Checking）[2-3]作為形式化驗(yàn)證的主要方法之一，以其較高的自動(dòng)化程度，近年來(lái)得到了學(xué)術(shù)界[4-5]和產(chǎn)業(yè)界[6-7]的廣泛關(guān)注。

SPIN[8-9]是由美國(guó)貝爾實(shí)驗(yàn)室開(kāi)發(fā)的一款著名的分布式系統(tǒng)模型檢測(cè)工具，目前已經(jīng)成功應(yīng)用于協(xié)議驗(yàn)證[10]、數(shù)據(jù)通訊、軟件驗(yàn)證及最優(yōu)規(guī)劃等領(lǐng)域。盡管SPIN 提供了對(duì)其建模語(yǔ)言Promela 的靜態(tài)語(yǔ)法檢查命令，但由于其并沒(méi)有集成一個(gè)高效的開(kāi)發(fā)環(huán)境，這種靜態(tài)檢查在復(fù)雜模型的建立中，存在明顯的滯后性。而且隨著SPIN 版本的更迭，其語(yǔ)法檢查命令和返回結(jié)果的格式發(fā)生了巨大變化，使得以往通過(guò)調(diào)用其自身命令實(shí)現(xiàn)的語(yǔ)法錯(cuò)誤反饋并不具有版本通用性。

本文通過(guò)對(duì)SPIN 內(nèi)核和Promela 文法[9-11]的進(jìn)一步研究，在Eclispe 平臺(tái)上設(shè)計(jì)實(shí)現(xiàn)了一個(gè)基于SPIN 的易擴(kuò)展的模型檢測(cè)環(huán)境——ESpin。該環(huán)境通過(guò)一個(gè)優(yōu)化了的代碼分區(qū)算法和可迅速支持SPIN 升級(jí)的文法分析器，構(gòu)造了一個(gè)高效、易擴(kuò)充的Promela 編輯器。編輯器除了支持Promela 的全部語(yǔ)法規(guī)則外，還提供了包括實(shí)時(shí)語(yǔ)法反饋、關(guān)鍵字高亮、大綱視圖、代碼折疊、代碼提示、代碼補(bǔ)全在內(nèi)的多種功能，提高了復(fù)雜模型的建模效率。此外，ESpin還為用戶(hù)提供多種運(yùn)行模式和特有的向?qū)А⑴渲媒缑?，?jiǎn)化了模型檢測(cè)的操作過(guò)程。

2 背景

2.1 SPIN 和Promela 建模語(yǔ)言

SPIN（Simple Promela Interpreter）[9]是美國(guó)貝爾實(shí)驗(yàn)室開(kāi)發(fā)的經(jīng)典分布式系統(tǒng)模型檢測(cè)工具。它以進(jìn)程為建模單位，通過(guò)進(jìn)程異步組合和系統(tǒng)空間窮舉驗(yàn)證等方式，模擬系統(tǒng)運(yùn)行，驗(yàn)證系統(tǒng)是否滿足指定的時(shí)序邏輯（LTL）和屬性規(guī)約，并在不滿足時(shí)輸出錯(cuò)誤軌跡，對(duì)錯(cuò)誤進(jìn)行定位。

Promela（Process or Protocol Meta Language）作 為SPIN 的采用的形式化建模語(yǔ)言，用來(lái)描述待測(cè)系統(tǒng)中各組件的自動(dòng)機(jī)模型。完整的Promela 模型由進(jìn)程、消息通道和變量組成[9]，其中進(jìn)程刻畫(huà)系統(tǒng)中并發(fā)實(shí)體的行為，消息通道和變量用來(lái)定義進(jìn)程運(yùn)行的環(huán)境。

2.2 Antlr和GNU Bison 工具

Antlr（Another Tool for Language Recognition）[12]是LL（k）文法的語(yǔ)法分析器生成器，通過(guò)讓用戶(hù)自定義詞法分析器和語(yǔ)法分析器的規(guī)則，生成相應(yīng)的詞法分析器和語(yǔ)法分析器的程序。它為Java、C++、C#等語(yǔ)言提供了一個(gè)通過(guò)語(yǔ)法描述來(lái)自動(dòng)構(gòu)造自定義語(yǔ)言的識(shí)別器、編譯器和解釋器的框架。

GNU Bison（簡(jiǎn)稱(chēng)Bison）[13]是屬于GNU 項(xiàng)目的一個(gè)通用文法分析器生成器，它能夠?qū)⒁粋€(gè)LALR（1）上下文無(wú)關(guān)文法的描述，轉(zhuǎn)換為一個(gè)可用做文法分析的C、C++或Java 解析器程序。在新版本中，Bison 還增加了對(duì)GLR（Generalized Left-to-right Rightmost）語(yǔ)法分析算法的支持。

由于Promela 語(yǔ)言在SPIN 的文法定義文件中被描述成LALR（1）文法，為了使構(gòu)造的文法分析器與SPIN 的描述嚴(yán)格一致，并且可隨著SPIN 的升級(jí)快速擴(kuò)充，選用Bison為編輯器構(gòu)造文法分析器。在詞法分析時(shí)，因常與Bison搭配使用的Flex 工具[13]不支持Java 語(yǔ)言的輸出，選用Antlr為其構(gòu)造相應(yīng)的詞法分析器。這樣經(jīng)過(guò)詞法分析和文法分析，文本中原本毫無(wú)意義的字符流就被整理構(gòu)造成程序?qū)?yīng)的符號(hào)表和抽象語(yǔ)法樹(shù)，用以實(shí)現(xiàn)實(shí)時(shí)語(yǔ)法反饋和代碼提示補(bǔ)全等功能。Promela 文法分析器的構(gòu)造過(guò)程將在4.2 節(jié)詳細(xì)描述。

2.3 相關(guān)工作

SPIN 作為一款著名的模型檢測(cè)工具，在學(xué)術(shù)界[14-15]和產(chǎn)業(yè)界[16-17]都得到了廣泛的應(yīng)用，針對(duì)其的平臺(tái)擴(kuò)展、工具擴(kuò)展和功能擴(kuò)展等的研究工作也一直在進(jìn)行。2005 年德國(guó)的Gerrit Rothmaier 團(tuán)隊(duì)首次實(shí)現(xiàn)了SPIN 工具在Eclipse平臺(tái)的擴(kuò)展[18]；2009 年馬里博爾大學(xué)的Tim Kov?e 團(tuán)隊(duì)在Eclipse 平臺(tái)上實(shí)現(xiàn)了SPIN 與st2msc（Spin Trail to Message Sequence Chart）的結(jié)合[19]。在后者的實(shí)現(xiàn)中，用戶(hù)通過(guò)手動(dòng)調(diào)用SPIN 的語(yǔ)法檢查命令，解析返回的字符串，來(lái)判斷建立的Promela模型是否存在語(yǔ)法錯(cuò)誤。

這些工作存在著兩個(gè)重要缺陷：（1）由于模型的復(fù)雜性，手動(dòng)的語(yǔ)法檢查不能及時(shí)地反饋出語(yǔ)法錯(cuò)誤，存在明顯的滯后性，為復(fù)雜模型的建立增加了難度；（2）隨著SPIN版本的更迭，自身命令返回的語(yǔ)法檢查結(jié)果在格式上發(fā)生了巨大變化，工具[19]在使用最新版本的SPIN 時(shí)，不僅不能正確標(biāo)記出模型中語(yǔ)法錯(cuò)誤的位置，反而會(huì)導(dǎo)致Eclipse 平臺(tái)的崩潰。

為了避免類(lèi)似問(wèn)題，在ESpin 環(huán)境的設(shè)計(jì)實(shí)現(xiàn)中，為編輯器構(gòu)造了一個(gè)通用的代碼分區(qū)算法，用來(lái)提高文本樣式化的效率，并依據(jù)SPIN 中對(duì)Promela 文法的定義[9]，構(gòu)造了一個(gè)可隨SPIN 升級(jí)快速擴(kuò)充的文法分析器，消除了SPIN版本變化對(duì)環(huán)境造成的影響。同時(shí)利用文法分析產(chǎn)生的符號(hào)表和抽象語(yǔ)法樹(shù)，實(shí)現(xiàn)了實(shí)時(shí)的語(yǔ)法反饋和更為精確的代碼提示補(bǔ)全等功能。

3 ESpin 模型檢測(cè)環(huán)境

3.1 設(shè)計(jì)思想

Eclipse 平臺(tái)[20]是開(kāi)放的富客戶(hù)端開(kāi)發(fā)平臺(tái)，它的所有功能集成都以擴(kuò)展點(diǎn)的形式存在。在其標(biāo)準(zhǔn)API[21]的基礎(chǔ)上實(shí)現(xiàn)了其對(duì)SPIN 工具的支持，提供了包括Promela 編輯器在內(nèi)的一整套模型檢測(cè)環(huán)境——ESpin。

在ESpin 環(huán)境中，對(duì)Eclipse 平臺(tái)現(xiàn)有的10 個(gè)擴(kuò)展點(diǎn)進(jìn)行了擴(kuò)充，以適應(yīng)模型檢測(cè)工作的需要，提供了Promela 語(yǔ)言的建模環(huán)境，以及SPIN 的配置、運(yùn)行、模擬、驗(yàn)證等基本操作。為了降低功能模塊之間的耦合性，將ESpin 環(huán)境主體劃分為4 部分：（1）外部數(shù)據(jù)導(dǎo)入模塊；（2）Promela 編輯器模塊；（3）可視效果優(yōu)化模塊；（4）模型檢測(cè)運(yùn)行模塊。每個(gè)模塊依據(jù)其功能特性選擇不同的擴(kuò)展點(diǎn)進(jìn)行擴(kuò)展，具體劃分如圖1 所示。

為了增強(qiáng)環(huán)境的擴(kuò)展性，降低不同檢測(cè)工具對(duì)整體環(huán)境的影響，為ESpin構(gòu)建了一個(gè)特殊的即插即用（Plug-and-Play）架構(gòu)。在這種架構(gòu)下，檢測(cè)工具與其建模語(yǔ)言的編輯器被直接關(guān)聯(lián)起來(lái)，作為一個(gè)可插拔的部分集成到環(huán)境中，而與環(huán)境的其他特性相對(duì)分離。當(dāng)需要在環(huán)境中使用其他檢測(cè)工具（如SMV）時(shí)，只要提供其對(duì)應(yīng)建模語(yǔ)言的編輯器，便可在現(xiàn)有環(huán)境基礎(chǔ)上，通過(guò)掛載的方式，輕松實(shí)現(xiàn)對(duì)其他工具的支持（如圖2 所示）。這種即插即用的架構(gòu)，降低了環(huán)境對(duì)SPIN 的依賴(lài)，使其不局限于單一工具，因而具有較強(qiáng)的擴(kuò)展能力，有助其成為Eclipse 平臺(tái)下通用的模型檢測(cè)環(huán)境。

圖1 ESpin 功能模塊與擴(kuò)展點(diǎn)圖

圖2 ESpin 的即插即用架構(gòu)圖

3.2 主要特性

正如前文所述，在Eclipse 平臺(tái)上實(shí)現(xiàn)的ESpin 模型檢測(cè)環(huán)境，主要包含以下7 個(gè)方面的特性：

（1）支持檢測(cè)工具和編輯器的快速擴(kuò)展；

（2）不受SPIN 升級(jí)的影響，可隨其升級(jí)快速擴(kuò)充，迅速實(shí)現(xiàn)向上兼容；

（3）支持Promela語(yǔ)言（6.0 版本）的全部語(yǔ)法和關(guān)鍵字，包括模型內(nèi)部的LTL 公式等特征；

（4）編輯器能實(shí)時(shí)反饋模型中的語(yǔ)法和語(yǔ)義錯(cuò)誤，并準(zhǔn)確標(biāo)記出錯(cuò)誤存在的位置；

（5）支持關(guān)鍵字高亮，大綱視圖，代碼折疊，代碼提示，代碼補(bǔ)全；

（6）提供了SPIN 的運(yùn)行、驗(yàn)證接口和另外兩種簡(jiǎn)捷的運(yùn)行模式；

（7）設(shè)計(jì)了一套ESpin 工程特有的透視圖和配置頁(yè)面，新增了ESpin 工程和Promela文件的新建、導(dǎo)入向?qū)А?/p>

在ESpin 環(huán)境中，用戶(hù)可以直接調(diào)用SPIN 的模擬和驗(yàn)證功能，運(yùn)行的結(jié)果將在Eclipse 控制臺(tái)打印出來(lái)。除常規(guī)模式之外，還提供了兩種更為簡(jiǎn)捷的運(yùn)行模式——運(yùn)行（Run）和復(fù)雜運(yùn)行（Verbose Run），使初學(xué)者也可以輕松使用，而不需要繁瑣的設(shè)置。當(dāng)然，同樣允許SPIN 的資深用戶(hù)，在環(huán)境的配置頁(yè)面對(duì)其模擬和驗(yàn)證的各項(xiàng)參數(shù)進(jìn)行精確的設(shè)置，更加高效地進(jìn)行模型的檢測(cè)工作。為了簡(jiǎn)化環(huán)境的設(shè)置過(guò)程，ESpin 還允許用戶(hù)自由地導(dǎo)入和導(dǎo)出自己的配置，以便在不同的主機(jī)上使用。ESpin 環(huán)境主要界面如圖3 所示。

圖3 ESpin 環(huán)境主要界面圖

4 Promela 編輯器

在模型檢測(cè)的過(guò)程中，大量工作都圍繞著抽象的系統(tǒng)模型展開(kāi)，一個(gè)功能全面、界面友好的編輯器能夠大大提高用戶(hù)的建模效率，使之更加專(zhuān)注于檢測(cè)本身。盡管之前的工作都提供了各自的Promela 編輯器，但是由于實(shí)現(xiàn)方式的原因，其文本的樣式化和語(yǔ)法錯(cuò)誤的反饋都存在明顯的滯后性，不能滿足復(fù)雜模型的建模需要。而且隨著SPIN的升級(jí)，利用其自身命令實(shí)現(xiàn)語(yǔ)法反饋的工具[19]甚至?xí)?dǎo)致Eclipse平臺(tái)的崩潰。

為了避免類(lèi)似問(wèn)題，實(shí)現(xiàn)更加高效準(zhǔn)確的代碼樣式化和語(yǔ)法反饋等功能，在Promela 編輯器的構(gòu)建中，設(shè)計(jì)實(shí)現(xiàn)了一個(gè)通用的代碼分區(qū)算法和一個(gè)可隨SPIN 升級(jí)快速擴(kuò)充的文法分析器，有效消除了SPIN版本變化對(duì)ESpin環(huán)境的影響。本章將對(duì)該代碼分區(qū)算法和Promela文法分析器進(jìn)行詳細(xì)介紹，并就功能和效率方面與同類(lèi)工作進(jìn)行細(xì)致比較。

4.1 通用的代碼分區(qū)算法

對(duì)任何編輯器來(lái)說(shuō)，都希望它能根據(jù)代碼的結(jié)構(gòu)對(duì)文本進(jìn)行必要的修飾，快速標(biāo)記出關(guān)鍵字和注釋等不同類(lèi)型的內(nèi)容。為實(shí)現(xiàn)這一過(guò)程，過(guò)去的工具往往都采用了重復(fù)掃描的方法：在輸入事件發(fā)生時(shí)，立即掃描整個(gè)文本，記錄全部關(guān)鍵字的位置，再用狀態(tài)機(jī)排除位于注釋和單雙引號(hào)內(nèi)的關(guān)鍵字，最后得到需要樣式化的部分。這種重復(fù)掃描的方式，雖然很容易理解和實(shí)現(xiàn)，但是當(dāng)模型較為復(fù)雜以及代碼長(zhǎng)度較大時(shí)，其處理速度必然會(huì)隨之降低。而且由于對(duì)編輯器的輸入大多都在文檔的尾部連續(xù)進(jìn)行，這種“先挑后揀”的策略本身就會(huì)造成大量的重復(fù)操作，降低了樣式化的效率。

為了解決此類(lèi)問(wèn)題，為編輯器設(shè)計(jì)了一個(gè)通用的代碼分區(qū)算法。該算法不僅適用于Promela 編輯器，而且可以在大多數(shù)同類(lèi)編輯器中使用。為了更清晰地描述算法過(guò)程，首先需要對(duì)用到的名詞概念進(jìn)行必要的說(shuō)明。

（1）字符組（Token）：用來(lái)存儲(chǔ)域和單詞符號(hào)的數(shù)據(jù)結(jié)構(gòu)，包含所存字符串的內(nèi)容、類(lèi)型，以及在編輯器中的位置等信息。

（2）文檔（Document）：編輯器中文本的全部?jī)?nèi)容，本質(zhì)上是一個(gè)字符串。

（3）域（Field）：由文檔分解而成，具有多種類(lèi)型。文檔被完全劃分為多個(gè)域，這些域互不相交，沒(méi)有重疊。全部的域構(gòu)成了整個(gè)文檔。一個(gè)域使用一個(gè)字符組存儲(chǔ)。

（4）單詞符號(hào)（Symbol）：由域依照掃描規(guī)則掃描而得。單詞符號(hào)可以是單詞、數(shù)值、符號(hào)和空格等。一個(gè)單詞符號(hào)使用一個(gè)字符組存儲(chǔ)。

（5）掃描規(guī)則（Rule）：將域分解為單詞符號(hào)的規(guī)則，用來(lái)識(shí)別域中特定的一組單詞或符號(hào)。

在構(gòu)造的代碼分區(qū)算法中，把域定義為5 種類(lèi)型：?jiǎn)涡凶⑨層颍⊿ingle-Line-Comments Field）、多行注釋域（Multi-Line-Comments Field）、字符域（Char Field）、字符串域（String Field）和代碼域（Code Field），用以滿足大多數(shù)語(yǔ)言樣式化的需要。不同類(lèi)型的域與不同的掃描器（scanner）相互綁定。為了在一次掃描中識(shí)別出更多的單詞符號(hào)，掃描器可以同時(shí)擁有多種掃描規(guī)則。這些規(guī)則包括：?jiǎn)卧~規(guī)則（WordRule）、字符規(guī)則（CharRule）、數(shù)值規(guī)則（NuberRule）和空格規(guī)則（WhitespaceRule）等。

具體的算法步驟描述如下：

（1）為對(duì)編輯器的操作創(chuàng)建一個(gè)編輯器事件（DocumentEvent）并判斷其類(lèi)型，若是打開(kāi)，轉(zhuǎn)步驟2，若是輸入，轉(zhuǎn)步驟3，若是關(guān)閉，轉(zhuǎn)步驟9。

（2）啟動(dòng)文檔分割器（FastPartitioner）掃描整份文檔，將文檔分解成多個(gè)不同類(lèi)型的域，返回這些域的字符組（List＜Token＞），轉(zhuǎn)步驟4。

（3）根據(jù)輸入的位置，啟動(dòng)文檔分割器對(duì)輸入所在的域和其后所有域進(jìn)行掃描，更新受到輸入影響的域（List＜Token＞），并將其返回。

（4）查看器（SourceViewer）啟動(dòng)外觀協(xié)調(diào)器（PresentationReconciler）。

（5）外觀協(xié)調(diào)器使用一個(gè)狀態(tài)機(jī)，根據(jù)域的類(lèi)型，把得到的字符組分配至對(duì)應(yīng)的掃描器。

（6）掃描器啟動(dòng)掃描線程，依照各自的掃描規(guī)則，識(shí)別域中的關(guān)鍵字，返回掃描結(jié)果即單詞符號(hào)的字符組（List＜Token＞）。

（7）啟動(dòng)樣式修復(fù)器（DefaultDamagerRepairer），為第（6）步產(chǎn)生的字符組按照預(yù)設(shè)的文本樣式（TextPresentation）進(jìn)行修飾。

（8）修飾完成后，掛起掃描器、樣式修復(fù)器和外觀協(xié)調(diào)器，等待下一次操作，轉(zhuǎn)步驟1。

（9）釋放掃描器、樣式修復(fù)器和外觀協(xié)調(diào)器，關(guān)閉文檔。

需要注意的是，在文檔分割器分割文檔時(shí)，會(huì)按照其域的類(lèi)型，將分割結(jié)果放入5 個(gè)序列（List）。整個(gè)樣式化流程如圖4 所示。

這一算法的優(yōu)勢(shì)在于，編輯器只需要在文檔打開(kāi)時(shí)對(duì)其進(jìn)行一次完整的掃描，而在之后的輸入中，只要重新掃描其中的部分域，就可以實(shí)現(xiàn)整個(gè)文本樣式化的更新。由于大多數(shù)情況下，對(duì)編輯器的輸入都在其末尾連續(xù)進(jìn)行，此時(shí)只要對(duì)位于文檔的最后一個(gè)域進(jìn)行再次掃描，就可以完成樣式更新，因此能夠大幅提高樣式化的效率。而且，對(duì)大多數(shù)語(yǔ)言來(lái)說(shuō)，只要為其中的代碼域設(shè)立掃描器，用來(lái)區(qū)分其中的關(guān)鍵字和其他內(nèi)容，就可以滿足需要，此時(shí)當(dāng)外觀協(xié)調(diào)器發(fā)現(xiàn)需要更新的域中沒(méi)有代碼域時(shí)，整個(gè)過(guò)程就可以停止，從一定程度上節(jié)省了時(shí)間和空間的開(kāi)銷(xiāo)。同時(shí)，這種“分而治之”的策略能夠完全排除文檔中無(wú)意義位置（如注釋中）關(guān)鍵字的干擾（因?yàn)椴辉谕粋€(gè)域中），也提高了代碼樣式化的精度。

4.2 Promela 文法分析器

在構(gòu)造的Promela 編輯器中，僅僅依據(jù)代碼結(jié)構(gòu)，進(jìn)行樣式上的修飾顯然是不夠的，尤其是當(dāng)模型較為復(fù)雜時(shí)，如果不能根據(jù)代碼的內(nèi)容動(dòng)態(tài)反饋出語(yǔ)法方面的錯(cuò)誤，建模必將會(huì)是個(gè)令人頭痛的過(guò)程。

圖4 文本樣式化流程圖

為了使編輯器具有這種能力，以往的工具大都采用了一種投機(jī)的方法：當(dāng)需要檢查語(yǔ)法錯(cuò)誤時(shí)，手動(dòng)調(diào)用SPIN提供的檢查命令，并對(duì)返回的結(jié)果字符串進(jìn)行解析，把解析得到的出錯(cuò)位置標(biāo)記在編輯器中。很顯然，這種手動(dòng)調(diào)用的方式，存在兩個(gè)重要缺陷：首先，在實(shí)際的建模工作中，手動(dòng)調(diào)用具有明顯的滯后性，不能及時(shí)地反饋語(yǔ)法錯(cuò)誤；其次，隨著SPIN 的升級(jí)，這種針對(duì)字符串的解析并不具有版本通用性。實(shí)際上，由于SPIN 版本的變化，工具[19]的字符串解析器不僅不能正確標(biāo)記出語(yǔ)法錯(cuò)誤的位置，反而會(huì)導(dǎo)致Eclipse平臺(tái)的崩潰。

為了在建模過(guò)程中能夠?qū)崟r(shí)感受到存在的語(yǔ)法錯(cuò)誤，并使這種能力不受SPIN 升級(jí)的影響，嚴(yán)格依照SPIN 的文法定義文件，為編輯器定制了一個(gè)特有的Promela 文法分析器，并依此實(shí)現(xiàn)了諸如實(shí)時(shí)語(yǔ)法反饋、代碼提示等功能。

由于Promela 在SPIN 中被描述成LALR（1）文法[9]，為了保證與定義的一致性，選用可接受該文法規(guī)則的Bison工具為編輯器構(gòu)造文法分析器（如圖5）。與常見(jiàn)的Flex 與Bison 的組合不同，因?yàn)镕lex 不接受Java 格式的輸出，該詞法分析器由Antlr 工具構(gòu)造。這種Antlr 與Bison 的組合可以直接接受SPIN 中的文法定義。在SPIN 升級(jí)時(shí)，如果Promela 文法沒(méi)有改變，則編輯器可以直接保證向上兼容，而不需要任何改動(dòng)；即使Promela 的文法被修改，也只要對(duì)文法分析器進(jìn)行簡(jiǎn)單的擴(kuò)充，便能迅速實(shí)現(xiàn)對(duì)新版本的支持，消除升級(jí)帶來(lái)的影響。

圖5 利用Bison 構(gòu)造文法分析器

由于SPIN 的開(kāi)發(fā)團(tuán)隊(duì)在文法定義文件中，不僅規(guī)定了Promela 的文法規(guī)則，還為其設(shè)定了語(yǔ)義動(dòng)作，因此在構(gòu)造文法分析器時(shí)，需要對(duì)其中的動(dòng)作進(jìn)行改寫(xiě)，以適應(yīng)文法分析的需要。圖5 是根據(jù)SPIN 文法描述構(gòu)造文法分析器的一段代碼，用來(lái)接受proctype 的定義。在這段代碼的中，Inst、proctype、Opt_priority、Opt_enabler 和body 都是非終結(jié)符。NAME、PROCTYPE 和D_PROCTYPE 是由Antlr 定義的token 類(lèi)型的名稱(chēng)（以標(biāo)識(shí)符命名）。大括號(hào)內(nèi)的語(yǔ)句是改寫(xiě)的文法分析的動(dòng)作。當(dāng)前面的語(yǔ)句被識(shí)別，動(dòng)作就被觸發(fā)執(zhí)行。在例子程序中，ErrorFind.CheckName 會(huì)先將NAME 聲明為proctype 類(lèi)型，然后查詢(xún)符號(hào)表判斷該符號(hào)是否已經(jīng)被定義。如果已被定義，則在NAME 處報(bào)錯(cuò)；否則把該符號(hào)加入到PROCTYPE 類(lèi)型的符號(hào)表中，并將NAME、decl、Opt_enabler 和body 節(jié)點(diǎn)添加到proc 節(jié)點(diǎn)下（ASTUtil.createNode）。圖6 是根據(jù)SPIN 的文法定義文件構(gòu)造的抽象語(yǔ)法樹(shù)（限于篇幅僅展示部分），圖5 的代碼段構(gòu)造了其中虛線圍起來(lái)的部分（sequence即為body）。

圖6 根據(jù)定義構(gòu)造的抽象語(yǔ)法樹(shù)

實(shí)際上，制定的文法分析動(dòng)作都包含了兩方面的內(nèi)容：一是檢查有沒(méi)有語(yǔ)法錯(cuò)誤，二是構(gòu)造相應(yīng)的抽象語(yǔ)法樹(shù)。構(gòu)造語(yǔ)法樹(shù)的過(guò)程相對(duì)簡(jiǎn)單，只需要建立節(jié)點(diǎn)和插入節(jié)點(diǎn)。而檢查語(yǔ)法錯(cuò)誤在不同的場(chǎng)合，則分為兩種情況：（1）在變量定義時(shí)，需要檢查所定義的符號(hào)（NAME）在符號(hào)表中是否已經(jīng)存在，如果存在則報(bào)錯(cuò)，否則將其添加到所屬類(lèi)型的符號(hào)表中；（2）在變量引用時(shí)，同樣檢查所引用的符號(hào)在符號(hào)表中是否已經(jīng)存在，不同的是，此時(shí)如果符號(hào)不存在則報(bào)錯(cuò)。為了加快符號(hào)表的檢索效率，依照符號(hào)的類(lèi)型將符號(hào)表分為3 張，分別記錄系統(tǒng)類(lèi)型（PROCTYPE）、自定義類(lèi)型（USERTYPE）和變量類(lèi)型（VARIABLE）的符號(hào)。因此在檢查語(yǔ)法錯(cuò)誤前，首先需要記錄符號(hào)的類(lèi)型和其他相關(guān)信息，然后才在相應(yīng)的符號(hào)表中檢索。具體的查錯(cuò)分析流程如圖7 所示。

圖7 查錯(cuò)分析流程圖

至此，經(jīng)過(guò)對(duì)Promela 字符流的詞法和語(yǔ)法分析，構(gòu)造出了程序?qū)?yīng)的符號(hào)表和抽象語(yǔ)法樹(shù)，編輯器許多基于內(nèi)容的功能都可以依靠它們得以實(shí)現(xiàn)。以代碼提示為例，當(dāng)用戶(hù)需要提示時(shí)，編輯器會(huì)解析文檔結(jié)構(gòu)，找出需要提示的符號(hào)名（如msg），然后在符號(hào)表中查找符號(hào)的類(lèi)型（如自定義類(lèi)型Message），通過(guò)對(duì)應(yīng)類(lèi)型的語(yǔ)法樹(shù)節(jié)點(diǎn)，遍歷查找所有的成員變量，生成建議列表并返回至編輯器顯示出來(lái)。

4.3 與同類(lèi)工作的比較

在ESpin 模型檢測(cè)環(huán)境的實(shí)現(xiàn)中，通過(guò)采用上文描述的優(yōu)化代碼分區(qū)算法和針對(duì)Promela 語(yǔ)言構(gòu)建的文法分析器，大幅提高了復(fù)雜模型代碼樣式化的效率，更為高效準(zhǔn)確地實(shí)現(xiàn)了諸如代碼提示、代碼補(bǔ)全、實(shí)時(shí)語(yǔ)法反饋等編輯器功能，有效降低了復(fù)雜模型的建模難度，提升了建模過(guò)程的工作效率。

盡管Eclipse 平臺(tái)為所有文件類(lèi)型都提供了默認(rèn)的文本編輯器，但該編輯器并不提供如樣式化、代碼提示等附加功能，因此在橫向比較中加入了ESpin 與JDT（Eclipse 下Java 開(kāi)發(fā)環(huán)境）的比較。在與同類(lèi)模型檢測(cè)環(huán)境的比較中，選取了功能較為全面的Eclipse Plug-in for Spin and St2msc Tools[14]（EPSST），此工具同樣基于Eclipse 平臺(tái)開(kāi)發(fā)，具有更強(qiáng)的可比性。ESpin 環(huán)境與原生Eclipse、JDT、EPSST 的功能性比較，如表1 所示。

從表1 可以看出，ESpin 環(huán)境由于具備針對(duì)Promela 語(yǔ)言的文法分析器，編輯器功能更加全面，針對(duì)代碼內(nèi)容的分析更加完善。目前，ESpin 環(huán)境支持的實(shí)時(shí)語(yǔ)法、語(yǔ)義反饋類(lèi)型包括：（1）不符合文法規(guī)范的錯(cuò)誤語(yǔ)句；（2）類(lèi)型引用錯(cuò)誤；（3）重復(fù)定義；（4）由作用域引起的跨界引用錯(cuò)誤；（5）LTL 規(guī)約公式錯(cuò)誤。在后續(xù)版本中，將增加對(duì)trace 不唯一，進(jìn)程數(shù)過(guò)多等語(yǔ)義錯(cuò)誤的實(shí)時(shí)標(biāo)記，以及對(duì)未被引用變量和不可達(dá)程序段等警告類(lèi)型的動(dòng)態(tài)反饋，繼續(xù)加強(qiáng)編輯器對(duì)Promela語(yǔ)言的支持，優(yōu)化用戶(hù)的建模體驗(yàn)。

性能方面，分別對(duì)1 000行、5 000行和10 000行的Promela代碼（JDT 對(duì)應(yīng)為Java 代碼）初次樣式化時(shí)間和樣式化維護(hù)時(shí)間進(jìn)行了統(tǒng)計(jì)，統(tǒng)計(jì)結(jié)果如圖8所示。結(jié)果表明，與EPSST“先挑后揀”的策略相比，ESpin 通過(guò)采用優(yōu)化的代碼分區(qū)算法，大幅減少了其在樣式化維護(hù)方面的開(kāi)銷(xiāo)，尤其是當(dāng)模型規(guī)模較大時(shí)，這一性能提升十分顯著。與JDT 相比，由于ESpin 掃描規(guī)則相對(duì)簡(jiǎn)單，且暫未對(duì)注釋域進(jìn)行二次掃描，代碼規(guī)模適中時(shí)，性能略好于JDT。值得說(shuō)明的是，JDT 采用的代碼分區(qū)算法僅適用于Java 語(yǔ)言，具有很強(qiáng)的語(yǔ)言局限性，與本文描述的通用分區(qū)算法有本質(zhì)區(qū)別。原生的Eclipse 平臺(tái)由于只提供簡(jiǎn)易的文本編輯器，而不具備代碼樣式化的功能，此處不參與比較。

表1 ESpin 環(huán)境與原生Eclipse、JDT、EPSST 的功能性比較

圖8 代碼樣式化時(shí)間比較

此外，還在ESpin 環(huán)境中測(cè)試了在文檔尾部輸入時(shí)其代碼樣式化與語(yǔ)法檢查更新的時(shí)間開(kāi)銷(xiāo)，以及總的響應(yīng)延遲，如圖9 所示。結(jié)果表明，ESpin 環(huán)境完全可以勝任較大規(guī)模的復(fù)雜模型建模工作。

圖9 ESpin 代碼樣式化與語(yǔ)法檢查更新效率

5 結(jié)束語(yǔ)

本文在Eclipse 平臺(tái)上設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)基于SPIN 的模型檢測(cè)環(huán)境——ESpin。該環(huán)境采用獨(dú)特的“即插即用”架構(gòu)，提供了一個(gè)功能全面、界面友好的Promela 建模和檢測(cè)環(huán)境，提高了復(fù)雜模型的建模效率。環(huán)境中集成的Promela 編輯器，通過(guò)一個(gè)優(yōu)化了的代碼分區(qū)算法和可隨SPIN 升級(jí)快速擴(kuò)充的文法分析器，更為高效準(zhǔn)確地實(shí)現(xiàn)了包括代碼樣式化，實(shí)時(shí)語(yǔ)法反饋，代碼提示補(bǔ)全在內(nèi)的多種功能，消除了SPIN 升級(jí)對(duì)環(huán)境帶來(lái)的影響。此外，環(huán)境還為用戶(hù)提供了多種運(yùn)行模式和特有的向?qū)渲庙?yè)面，使初學(xué)者也能輕松使用。

在下一步的工作中，將繼續(xù)完善編輯器對(duì)多Promela文件交互方面的支持，為SPIN 不同的運(yùn)行模式增加新的圖形界面，使用戶(hù)更加直觀地感受運(yùn)行時(shí)的數(shù)據(jù)交互情況。

致謝感謝南京航空航天大學(xué)軟件質(zhì)量保障與測(cè)試技術(shù)研究生主題創(chuàng)新實(shí)驗(yàn)室對(duì)本研究課題的大力支持。

[1] Holzmann G.Formal software verification：how close are we?[J].Formal Techniques for Distributed Systems，2010（1）.

[2] Merz S.Model checking：a tutorial overview[J].Modeling and Verification of Parallel Processes，2001，2067：3-38.

[3] Jhala R，Majumdar R.Software model checking[J].ACM Computing Surveys（CSUR），2009，41（4）.

[4] Chen Z.On the generative power of ω-grammars and ω-automata[J].Fundamenta Informaticae，2011（2）：119-145.

[5] Chen Z，Motet G.Nevertrace claims for model checking[C]//Proceedings of the 17th International SPIN Workshop on Model Checking Software，2010：162-179.

[6] Chen Z，Motet G.Methodology and experience for designing safety-related systems in IEC 61508[C]//Proceedings of the 4th Conference on Dependa-Bility，2011：57-64.

[7] Chen Z，Motet G.Towards better support for the evolution of safety requirements via the model monitoring approach[C]//Proceedings of the ACM/IEEE 32nd Conference on Software Engneering（ICSE2010）.[S.l.]：IEEE Computer Society Publishers，2010：219-222.

[8] Holzmann G J.The model checker SPIN[J].IEEE Transactions on Software Engineering，1997，23（5）：279-295.

[9] Holzmann G J.The SPIN model checker：primer and reference manual[M].[S.l.]：Addison-Wesley，2004.

[10] Chen Z，Zhang D，Zhu R，et al.A review of automated formal verification of ad hoc routing protocols for wireless sensor networks[J].Sensor Letters，2012（12）.

[11] Holzmann G J.Promela language reference[J].Bell Labs，1997（5）.

[12] Parr T，Lilly J，Wells P，et al.ANTLR reference manual[R].MageLang Institute，2000-01.

[13] Levine J.Flex & bison[M].[S.l.]：O’Reilly Media，Inc，2009.

[14] Jiang K，Jonsson B.Using SPIN to model check concurrent algorithms，using a translation from C to Promela[D].Uppsala，Sweden：Uppsala University，2009.

[15] 徐丙鳳，胡軍，曹東，等.T-CBESD：一個(gè)構(gòu)件化嵌入式軟件設(shè)計(jì)模型驗(yàn)證工具[J].小型微型計(jì)算機(jī)系統(tǒng)，2010，31（11）.

[16] Havelund K，Lowry M，Penix J.Formal analysis of a space-craft controller using SPIN[J].IEEE Transactions on Software Engineering，2001，27（8）：749-765.

[17] De Vries R G，Tretmans J.On-the-fly conformance testing using SPIN[J].International Journal on Software Tools for Technology Transfer（STTT），2000，2（4）：382-393.

[18] Rothmaier G，Kneiphoff T，Krumm H.Using Spin and Eclipse for optimized high-level modeling and analysis of computer network attack models[J].Model Checking Software，2005，3639：903-904.

[19] Kov?e T，Vlaovi? B，Vre?e A，et al.Eclipse plug-in for spin and st2msc tools-tool presentation[J].Model Checking Software，2009，5578：143-147.

[20] Clayberg E，Rubel D.Eclipse：building commercial-quality plug-ins（Eclipse）[M].[S.l.]：Addison-Wesley Professional，2006.

[21] Help-Eclipse Platform[EB/OL].[2012-07-01].http：//help.eclipse.org/.