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

南京航空航天大學 計算機科學與技術學院，南京210016

1 引言

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

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

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

2 背景

2.1 SPIN 和Promela 建模語言

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

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

2.2 Antlr和GNU Bison 工具

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

GNU Bison（簡稱Bison）[13]是屬于GNU 項目的一個通用文法分析器生成器，它能夠將一個LALR（1）上下文無關文法的描述，轉換為一個可用做文法分析的C、C++或Java 解析器程序。在新版本中，Bison 還增加了對GLR（Generalized Left-to-right Rightmost）語法分析算法的支持。

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

2.3 相關工作

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

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

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

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

3.1 設計思想

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

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

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

圖1 ESpin 功能模塊與擴展點圖

圖2 ESpin 的即插即用架構圖

3.2 主要特性

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

（1）支持檢測工具和編輯器的快速擴展；

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

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

（4）編輯器能實時反饋模型中的語法和語義錯誤，并準確標記出錯誤存在的位置；

（5）支持關鍵字高亮，大綱視圖，代碼折疊，代碼提示，代碼補全；

（6）提供了SPIN 的運行、驗證接口和另外兩種簡捷的運行模式；

（7）設計了一套ESpin 工程特有的透視圖和配置頁面，新增了ESpin 工程和Promela文件的新建、導入向導。

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

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

4 Promela 編輯器

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

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

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

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

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

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

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

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

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

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

在構造的代碼分區(qū)算法中，把域定義為5 種類型：單行注釋域（Single-Line-Comments Field）、多行注釋域（Multi-Line-Comments Field）、字符域（Char Field）、字符串域（String Field）和代碼域（Code Field），用以滿足大多數(shù)語言樣式化的需要。不同類型的域與不同的掃描器（scanner）相互綁定。為了在一次掃描中識別出更多的單詞符號，掃描器可以同時擁有多種掃描規(guī)則。這些規(guī)則包括：單詞規(guī)則（WordRule）、字符規(guī)則（CharRule）、數(shù)值規(guī)則（NuberRule）和空格規(guī)則（WhitespaceRule）等。

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

（1）為對編輯器的操作創(chuàng)建一個編輯器事件（DocumentEvent）并判斷其類型，若是打開，轉步驟2，若是輸入，轉步驟3，若是關閉，轉步驟9。

（2）啟動文檔分割器（FastPartitioner）掃描整份文檔，將文檔分解成多個不同類型的域，返回這些域的字符組（List＜Token＞），轉步驟4。

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

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

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

（6）掃描器啟動掃描線程，依照各自的掃描規(guī)則，識別域中的關鍵字，返回掃描結果即單詞符號的字符組（List＜Token＞）。

（7）啟動樣式修復器（DefaultDamagerRepairer），為第（6）步產(chǎn)生的字符組按照預設的文本樣式（TextPresentation）進行修飾。

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

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

需要注意的是，在文檔分割器分割文檔時，會按照其域的類型，將分割結果放入5 個序列（List）。整個樣式化流程如圖4 所示。

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

4.2 Promela 文法分析器

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

圖4 文本樣式化流程圖

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

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

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

圖5 利用Bison 構造文法分析器

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

圖6 根據(jù)定義構造的抽象語法樹

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

圖7 查錯分析流程圖

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

4.3 與同類工作的比較

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

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

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

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

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

圖8 代碼樣式化時間比較

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

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

5 結束語

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

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

致謝感謝南京航空航天大學軟件質量保障與測試技術研究生主題創(chuàng)新實驗室對本研究課題的大力支持。

[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：一個構件化嵌入式軟件設計模型驗證工具[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/.