基于Event-B的軟件工程形式化方法綜述①

彭 寒,張曉麗,劉洲洲,曹國震,景月娟,王 瑾,李添銳

1(西安航空學院 計算機學院,西安 710077)

2(西安石油大學 計算機學院,西安 710065)

1 引言

隨著物聯網、云計算、信息物理融合系統時代的到來,“軟件定義”已成為當前計算機科學以及軟件學科的研究熱點.軟件的泛在化導致軟件系統的規模日漸龐大,復雜度不斷攀升,讓軟件設計和驗證的難度不斷增長.為應對軟件設計、開發和驗證中的復雜性,國內外研究團隊不斷提出新的、先進的軟件設計與驗證理論來提升軟件開發效率、保證軟件制品的安全性和可靠性.軟件工程的形式化方法[1]是目前最有前景的軟件開發方法之一.在形式化方法的支持下,研究人員能夠使用嚴格的數學模型來描述系統的需求,并驗證給定的系統或系統模型是否滿足所要求的行為屬性[2].雖然形式化方法已經被證明是保證系統的正確性和一致性的良好方法,但是其在軟件工程中的應用一直無法大范圍推廣.其原因在于形式化方法的學習成本較高、可理解性差,且形式化模型在結構化、模塊化和復用性方面存在一定局限.

Abrial 等發明的Event-B[3]是目前最貼近軟件工程的一種形式化語言,其逐步精化的思想和自動代碼生成的能力,不僅保證了模型的正確性和一致性,同時又能對軟件開發的全壽命周期提供良好的支持.Event-B 方法已經成為支持軟件工程形式化的主要方法之一.

本文首先對已有的基于Event-B的軟件工程形式化方法進行了分類闡述,主要分為Event-B 模型的控制結構、面向對象的Event-B 模型、可重用的Event-B 模型、實時Event-B 模型.而后對基于Event-B的軟件工程形式化方法的未來發展方向提出了預測和建議;最后對本文內容進行總結.

2 基于Event-B的軟件工程形式化方法現狀分析

2.1 Event-B 模型的控制結構

Hallerstede 等[4]指出,Event-B在結構化建模方面的一個重要缺陷就是無法提供描述事件發生次序的機制,也就是無法表達系統的控制流.為了對事件排序,通常需要在Event-B 模型中額外的構造一個抽象計數器.Hallerstede 等認為主要原因在于Event-B為了達到最簡化的符號系統,過多的舍棄了B 方法中的大量的控制結構.因此,原生的Event-B 模型的控制流通常都是不可見的,因為一個Event-B 模型中的事件都是“平坦”的,建模者看到的就是一個大的事件集合,既沒有像UML 或者SysML 那樣將系統分解為子系統、構件、對象,也沒有像序列圖、流程圖那樣易理解的符號系統來表達事件之間的關系.為解決這個問題,研究人員在這方面所做的工作包括邊精化和節點精化、事件精化結構、流語言以及CSP||B 方法.

(1)邊精化和節點精化

為了能夠清晰地表達Event-B 模型的事件次序,Hallerstede 等介紹了一套結構化的符號來描述Event-B 模型的3 種基本結構(step,loop,choice)[4]和1 種復合結構box.在其符號系統中,采用斷言作為節點,并用事件在轉換邊上標記.采用這種方法,能夠讓Event-B 模型中的事件次序變得更加清晰,同時也能夠讓不變式變得更加簡單.在此基礎上,Hallerstede 等在文獻[5]中提出了對狀態轉換系統進行精化的兩種方法:邊精化和節點精化.從Event-B 模型的角度來說,邊精化就是對事件的分解,將一個事件分解為幾個子事件;而節點精化則是對狀態的精化,是將一個抽象狀態精化為幾個具體的狀態.

Hallerstede 等的工作[4,5]為Event-B 模型的控制結構提供了很好的建議和思路,但是并沒有提供顯式的圖形化工具來支持Event-B的控制流建模.但是邊精化和節點精化的思想為后續的各種Event-B 控制結構表示方法提供了理論指導.

(2)事件精化結構

Butler[6]首先提出了事件精化圖的思想,希望能夠用Jackson 結構圖的風格來表達Event-B 模型中抽象事件和精化事件之間的關系.Fathabadi 等[7]在此基礎上提出了3 種基本的原子分解結構,分別為:(1)順序結構,表示抽象事件被分解為幾個順序執行的精化事件;(2) or 結構,表示抽象事件被分解為幾個可能的精化事件;(3)循環結構,表示精化事件被分解為一個能夠多次重復執行的精化事件.Fathabadi 等將這種方法應用于多媒體協議的開發,并指出,在建立大型復雜系統的Event-B 模型時,精化層次過多必然會讓模型的復雜度提升,而原子分解方法可以在一定程度上緩解這種復雜性.隨后,Fathabadi 等[8]在建立水星探測系統的Event-B 模型時,又提出了事件原子分解的Xor結構和All 結構,分別表示“抽象事件被分解為不可能同時發生的多個精化事件”以及“抽象事件被分解為一系列必須全都發生的精化事件”,并為原子分解模式添加了多實例的情況.2012年,Fathabadi 等[9]將原子分解方法正式命名為AD (Atomicity Decomposition)方法,并定義了原子分解語言ADL (Atomicity Decomposition Language)來描述原子分解模式;同時,Fathabadi 等采用模型轉換技術,將ADL 定義的原子分解模式轉換為對應的Event-B 模型.Fathabadi在他的博士論文[10]中,對其工作做了總結,共提出了8 種事件分解模式,包括5 種控制流模式Sequence 模式、Loop 模式、And 模式、Or 模式、Xor 模式和3 種Replicator 模式:All 模式、Some 模式和One 模式.

此后,南安普頓大學的Alkhammash 等[11]將AD 方法和UML-B 方法結合,提出了一種綜合結構化精化和控制流精化的Event-B 模型構建方法,將需求劃分為面向數據的需求、面向事件的需求、面向約束的需求、面向控制流的需求以及其它需求.它使用UML-B 來建模面向數據的需求,并使用AD 方法來建模面向控制流的需求.采用UML-B和AD 方法就可以覆蓋整個系統需求建模,并保證需求的可追溯性;同時還提出了AD 方法不僅能夠描述多級精化模型中的事件精化關系,還能夠表達控制流需求.

Fathabadi 等持續改進AD 方法,并將其重新命名為ERS (Event Refinement Structure)方法[12],將AD 插件做了進一步的完善,變為ERS 插件.

事件精化結構的優勢在于,系統建模人員可以從宏觀上評估各種精化結構的優劣,為評估不同的系統精化策略提供依據.同時AD/ERS 圖形化插件所表達的事件精化結構可以生成大部分的Event-B 控制流代碼,免除了建模人員的手工編碼負擔.

事件精化結構的局限在于,它更適合表達各精化層級之間的靜態的精化關系,也就是事件精化的靜態結構.在表達系統的動態行為方面,AD/ERS 方法所使用的樹形結構圖并不直觀.AD/ERS 方法的另一個局限就是很難映射到類似CSP 或者LTS 這樣的行為語義模型上,因此也就難以方便的驗證模型的行為屬性.

(3)流語言

紐卡索大學的Iliasov[13]提出了一種不修改Event-B 模型而對其施加控制流約束的方法,稱之為流語言.流語言采用ena、dis、和fis 分別表達一個事件使能下一個事件,一個事件不使能下一個事件,以及一個事件可能會使能下一個事件;進一步的,流語言采用And,Or和Xor 來表達事件之間的并發、“非排斥或”和“排斥或”關系,從而得到了一個結構化的語言,以支持對Event-B 模型的事件順序的建模和驗證.Iliasov用流插件提供了圖形化的符號來建模事件序列.從圖形含義的角度來說,流插件用節點表達事件,而用遷移來表達事件之間的使能(enable)關系.

流語言的優勢在于,它能直接用平面的圖形來表達事件之間的觸發-響應關系,也就是事件的發生次序,從這個角度來說,它比AD/ERS 方法更好.同時它也提供了并發事件和互斥事件的表達方式,對并發程序的建模提供了支持.

流語言的局限性也很明顯,那就是它所采用的事件-觸發形式的控制流表達方式與通用的狀態轉換系統的符號不一致,要將其轉換為某種行為語義模型,還需要做大量的轉換工作.另外,流插件存在的另一個問題是,它希望添加一個語法糖來修改Event-B 本身的語法,例如inc.*(double).這就修改了Event-B的語法結構,使得模型更加難以理解.

(4)CSP||B

正如Hallerstede 等指出的[4],Event-B的缺陷之一是沒有提供表達事件次序的機制,即,它無法表達系統的控制流.從某種意義上說,AD/ERS 方法、iUML-B狀態機和Flow 方法都可被視為是一種控制流建模語言.但是這些建模語言都不是嚴格的形式化的控制流模型.為了對Event-B的控制流進行形式化的建模,研究人員提出了一些方法,其中最典型的就是CSP||B 方法,其初衷是為經典B 提供控制流語義[14].由于CSP是一種進程代數,具有明確的行為語義,且CSP 中的失效-發散語義與Event-B 模型中的相應事件類型極其類似,因此CSP||B是一種非常適用于Event-B的行為語義模型.

Butler[15]主持開發了從CSP 轉換到經典B的工具csp2B.其主要思路是使用CSP 表達經典B 中的事件次序,而用經典B 表達事件的計算部分.csp2B 將CSP 控制模型轉換為經典B 之后,能夠自動生成證明責任,以保證模型的一致性.這樣,經典B 模型的精化就可以使用CSP 或者CSP和B的結合來完成.系統模型的行為精化由CSP 來保證,而動作精化(也就是數據精化) 由B 模型來保證,最終的系統模型就是CSP 模型和B 模型的組合,因此這種方法又被稱為CSP||B.Treharne 等[16]對CSP||B 方法進行了改進,讓CSP 進程和B 模型中的事件的隔離性更強.隨后,Butler 又對經典B的模型檢查工具ProB 進行了改進[17],讓其能夠檢查CSP和B 編寫的組合規約的一致性,并能夠檢查使用純粹的B 編寫的規約是否滿足用CSP描述的事件跡.Schneider和Treharne[18,19]對CSP和B 模型組合后的系統性質進行研究,提出了一種保證組合后的模型不會發散的約束.Colind 等[20]使用前述的CSP||B 方法,采用自底向上的方式,用B 模型表達計算部件,而用CSP 表達系統的執行流程,成功的開發了一個車輛自組織系統的形式化模型,證明了編寫和檢查CSP||B 規范可以幫助消除程序集及其通信協議中的錯誤和歧義.由于CSP和經典B的失效-發散語義類似,因此CSP 也被用來作為B的行為精化框架[21],以保障在B 模型的精化過程中能夠保持所需的行為屬性.

在Event-B 逐漸推廣之后,研究人員的關注點轉移到了如何結合CSP和Event-B 來開發系統的形式化模型.Schneider和Treharne 使用CSP 作為Event-B的控制流建模語言,從而使Event-B 模型中的控制流變得明確和清晰,從而增強可讀性,也便于分析.同時,這種方法也簡化了Event-B 模型中的大量的涉及控制流的規約代碼[22].更重要的是,Schneider 等提出了一個行為組合框架,證明了獨立的CSP||B 組件的精化模型在組合之后,得到的組合模型行為也是原來的抽象模型的行為的精化.Schneider 等用一個超時重傳協議的模型的案例證明了這種方法的優勢[23].與經典B 一樣,Event-B 也可以用CSP 作為它的行為語義模型,從而保證Event-B的精化鏈中的行為屬性(如安全性屬性)不被違背[24].Schneider 等證明了,只要CSP 控制流模型是無死鎖的,而Event-B 功能模型是非發散的,則這兩個模型的組合獲得的模型是無死鎖的[25].

CSP||B 方法的優勢在于它直接使用形式化的行為建模語言CSP 來建立Event-B 模型的控制流,使得Event-B 模型的行為屬性驗證更加簡單.

CSP||B 方法的局限在于,它要求建模人員必須精通兩種不同的形式系統,提升了學習成本,對建模人員的理論水平要求較高.

在各種Event-B 控制流建模方法中,邊精化/節點精化方法、事件精化結構合流語言有一些共性的內容,都將順序、選擇、循環和并發結構加入到了Event-B 模型中.這些方法的優點在于采用了各種(圖形化的或非圖形化的)方式讓Event-B 模型的控制流變得更加清晰,其自動生成的控制流代碼也免去了手工編寫模型的負擔,減少了人為引入的錯誤.但是這些方法都有一個重大的缺陷,即,它們都沒有給Event-B 模型的控制流賦予行為語義.因此,對Event-B 模型的行為屬性驗證仍然需要大量的、手工的交互式證明.CSP||B方法最大的優點是為Event-B 模型賦予了行為語義.因此,CSP||B 方法不僅能夠更清晰的表達Event-B 模型的控制流、并根據CSP 模型生成Event-B的控制流代碼,支持組合精化,而且還能夠為Event-B 模型的精化策略提供指導.讓Event-B 模型在精化過程中保證其行為屬性,如安全性、活性以及其他各種線性時態邏輯LTL (Linear Temporal Logic)屬性[26-28].而這種能力是其它3 種方法無法保證的.

Event-B對控制結構提供支持的方法的總結如表1所示.

表1 Event-B 模型的控制結構方法總結

2.2 面向對象的Event-B

面向對象方法一直是結構化設計和增強軟件模塊內聚性的公認的方法,用于體現面向對象的系統分析與設計思想的統一建模語言UML 也已被廣大工程人員所接受.Event-B的研究人員為推進Event-B在工程方面的應用,提出了一系列的綜合UML和Event-B的方法,為Event-B 模型的結構化做出了貢獻.

南安普頓大學的Snook 等在Event-B的UML 表達方面所做的工作最為杰出.Snook 等首先用UML Profile[29,30]構造了從UML的類圖和狀態圖到經典B的翻譯器;由于UML 本身非常復雜,所以Snook 等僅針對UML 中的類圖和狀態機設計了相應的翻譯器,可以將類和類之間的各種關聯關系,例如繼承、引用等映射到經典B 模型中的集合、變量和關系上;同時,UML-B 可以將狀態機映射到經典B 語言中的狀態變化上.為了表達程序的控制流和并發執行,UML-B 還使用了UML 活動圖中的一些建模元素,例如Fork、Join,偽狀態節點等,這些節點的添加也會影響到所生成的經典B的代碼.

隨著Event-B 取代經典B 成為主流的軟件系統建模語言,Snook 等又對UML-B 做了改進,定義了UML-B的正式的元模型[31].這使得UML-B 能夠更好地為Event-B 服務,而不是迎合UML的各種建模符號,也使得UML-B 變成了一種“類似于UML”的獨立的形式化建模語言.這一變化帶來的最重要的影響是,在此以后,UML-B 模型的結構、精化就代表了(或者說,就是)整個Event-B 模型的結構和精化,而不是像Profile機制那樣讓Event-B 作為UML 精化的附屬品.而UML-B的結構和精化問題也就成為了一個獨立的問題,和UML 中的類圖和狀態圖的精化區別開來.當然,UML-B的類圖和狀態機形式的圖形化表達方式和Event-B的文本形式的模型在結構化和精化方面還是存在直覺上的差距.為此,Snook 等專注于研究如何用UML-B的精化來表達Event-B 模型的精化,他和Hallerstede 一起研究了如何用UML-B 狀態機來表達狀態轉換圖的邊精化和節點精化問題,認為可以用層次化的狀態機來模擬添加到狀態空間和相應事件的細節(即節點精化),并用choice 偽狀態節點來表達事件的分解(即邊精化).Snook 等將這兩種精化分別稱為數據精化和事件精化[32].Said 等在Snook 工作的基礎上,提出UML-B 應該支持5 種精化方式:在精化類中添加新的屬性和關聯、在精化Machine 中添加新的類、狀態精化、轉換精化和事件在類之間的移動,并對UMLB 進行了擴展,使之支持這5 種精化方式[33,34].

UML-B的優點體現在:首先,它的出現和發展對基于Event的軟件工程形式化方法提供了強有力的支撐.由于UML-B 能夠自動生成文本形式的Event-B 模型,所以模型生產速度更快,因此對問題領域的探索更加方便,這一點非常有助于熟悉UML的工程人員盡快建立問題域的抽象的形式化模型,而不用糾結于形式化的數學語言[35].其次,UML-B 采用層次化的狀態機逐步完成模型的精化,在一定程度上隱藏了底層的實現細節,符合軟件開發人員的思維習慣;最后,通過其建模案例的研究,Said 等證明了[36,37],使用UML-B 精化比使用Event-B 精化更容易完成精化的正確性證明,這充分體現了Event-B 模型的結構化能夠在一定程度上降低形式化模型建模和驗證的復雜性.

UML-B的局限性包括:首先,類圖和狀態圖的粒度過細,對于復雜系統來說,會有過多的交互和控制流需要表達.其次,UML-B 模型無法與已有的Event-B machine 集成;最后,UML-B 狀態機表達方式無法表達并行的狀態機.

為解決UML-B的缺點,南安普頓大學對UMLB 持續地改進,使之能夠嵌入到傳統的Event-B 模型代碼中,并將現存的Event-B 模型中的事件與狀態機中的事件“鏈接”起來,從而達到控制事件次序的效果.目前,UML-B 已經發展為“集成的UML-B”(integrated UML-B,iUML-B),并已應用于各領域的系統建模[38].iUML-B 狀態機的另一個重要的優勢就是引入了并發狀態機,為直觀地建模并發系統提供了支持.

2.3 可重用的Event-B 模型

形式化模型,尤其是以定理證明方法為基礎的形式化模型,通常需要建模人員手工完成大量的證明,以保證模型的正確性和精化的一致性.因此,如何減小手動證明和交互式證明的工作量,提升形式化模型的可重用性,也是軟件工程形式化方法的一個重要研究領域.

(1)基于接口的Event-B 模型

依賴于接口而不是依賴于實現,是系統分層設計、獨立演化的基本策略,也是增強模型的復用性和擴展性的基本原則.紐卡索大學的Iliasov和奧博學術大學的Troubitsyna 等提出了基于接口的Event-B 模型設計策略,稱之為Modularisation 方法[39],其思路是將Event-B 模型分解為一個個的模塊,每個模塊由模塊接口和模塊實現構成.模塊接口包含了與環境交互的外部變量定義、不變式定義和操作定義;模塊的實現則是一個Event-B machine.模塊實現用事件來完成模塊接口中所定義的操作,而模塊的使用者調用模塊接口來使用模塊的服務.Modularisation 方法被應用于歐盟第七框架的衛星姿態和軌道控制系統的建模和驗證[40,41].進一步的,Modularisation 方法已被用于契約式的形式化模型的設計[42],從系統的形式化的Event-B 模型導出每個組件的契約,從而保證組件實現的互操作性.

基于接口的Event-B 模型的優勢是分離了Event-B模型的接口描述和接口實現,達到了形式化模型的接口與實現分離.由此而帶來的好處包括:支持Event-B模型的架構設計和推理;各模塊的實現可以獨立完成,而不用關注其他模塊的變化;提升了Event-B 模型的可擴展性等.同時,基于接口的Event-B 模型也解決了多層、多模態的控制系統中模式一致性難以驗證的問題,并利用架構分解的方法降低了大型復雜系統的形式化模型的復雜度.

基于接口的Event-B 模型的局限性在于,它對形式化模型的設計者的經驗有著更高的要求.接口一旦定義,就無法在后續的過程中隨意修改.因為后續的精化都必須符合接口的需求.這從某種程度上限制了形式化模型的設計者對設計空間的探索.

(2)基于組件的Event-B 模型

無論是原子分解、UML-B 還是基于接口的設計,都是為自頂向下的形式化建模提供支持.而在自底向上的形式化模型重用方面,還很少有人開展工作.芬蘭圖爾庫計算機科學中心的Edmunds和Snook 等合作,提出了使用已有的形式化組件庫來逐步構建系統形式化模型的方法[43-45].Edmunds 擴展了iUML-B的類圖,提出了接口類,并用組件實例圖來表達組件之間的組合.組件實例圖方法借鑒了CSP的組合語義,將Event-B的事件分為輸入事件、輸出事件這種與外部產生交互的接口事件以及不會與外部交互的內部事件,并沿用了CSP的組合規則,即兩個組件在共享事件上同步組合,組合后的事件對外部不可見,所形成的新的較大的組件就隱藏了共享事件,這樣,對于更高的層級來說,共享事件就變成了一個靜默的事件(τ 事件).

圖爾庫計算科學中心的Ostroumov 等也在Edmunds的工作的基礎上提出了一套可視化的Event-B 組件庫[46],設計了通用的Event-B 組件模型和連接器模型.其中,Event-B 組件模型包括環境事件和功能性事件,環境事件負責和外部環境交互,又被分為輸入事件和輸出事件,而功能事件負責將輸入事件讀入的數據進行處理,并傳遞給輸出事件.Event-B 連接器模型包括順序連接器模型和平行組合連接器模型.順序連接器負責兩個組件的數據交互,而平行組合連接器則完成兩個組件的行為同步.Ostroumov 等最終設計和實現了一個可視化的形式化組件庫[47],讓用戶可以直接用“dragand-drop”的方式直接使用已有的形式化組件庫來構建系統的形式化Event-B 模型,并用該組件庫搭建了一個液壓傳動系統和一個軌道交通控制系統的Event-B模型.

基于組件的Event-B 模型的優勢在于它實現了大粒度的形式化模型的重用,讓系統建模人員能夠采用快速地搭建大型系統的形式化模型,也達到了證明過程的重用.其局限性在于,領域組件庫中的形式化組件的專用性太強,目前只開發了液壓傳動系統和軌道交通控制系統的形式化組件庫.其他領域的建模人員必須自行開發新的組件庫,才能實現自底向上的系統建模過程.

(3)Event-B 設計模式

設計模式是軟件工程中實現軟件設計思想重用的重要方法,可以被視為是微型的、可重用的軟件體系結構模型.為提高Event-B 模型的可重用性,研究人員也提出了Event-B 設計模式的概念[48].Silva 等[49,50]提出了設計模式和“Generic Instantiation”的方法,并用這種技術完成了安全關鍵的地鐵系統的Event-B 模型的開發.在設計模式的實例化過程中,Generic Instantiation方法可以使用重命名插件來完成設計模式的實例化,在設計模式中已經完成的證明責任是無需重復證明的.Yeganefard 等[51]在將Monitored,Controlled,Mode and Commanded (MCMC)方法應用于Event-B 模型的過程中,提出了Event-B 模型的monitor 模式 control 模式,mode 模式和command 模式,在構建實際的控制系統的Event-B 模型時,只需要將這4 種事件模式實例化為實際的系統事件即可.Yeganefard 等使用MCMC的4 種模式開發了巡航控制系統[52]、汽車車道偏離預警系統[53]、車道對中控制器(LCC)[54]的Event-B 模型.在Yeganefard 等的工作中,提出了模式組合的方法,將簡單模式組合后形成組合模式.但是模式的組合需要工具的支持.除了以上典型的Event-B 設計模式之外,Gondal 等[55,56]提出了一些針對Event-B的精化模式和分解/組合模式,用于面向特征的控制系統的產品線的形式化建模.Intana[57]使用Event-B 設計模式建模了無線傳感器網絡中的精化和組合模式.

Event-B 設計模式的優勢在于,它抽象了某一個領域內的共性問題并將其表述為抽象的形式化模型,然后證明該模型的正確性.這樣建模人員就能夠采用重命名的方式直接將抽象模型實例化為具體問題的形式化模型,不僅避免了“重復的制造輪子”,也節省了重復的精化和正確性證明.但是Event-B 設計模式也存在一些局限.和基于組件的Event-B 一樣,設計模式本身都是針對某個領域的特定問題的共性抽象,因此每個設計模式所適用的領域也較為固定,難以直接應用于其他領域.

(4)Event-B 抽象數據類型

作為一種支持代碼生成的形式化建模語言,Event-B必然要支持對各種抽象數據類型,如線性表、堆棧、隊列和樹的自定義和可重用技術.Abrial和Butler 很早就提出了對Event-B 進行數學擴展的思路[58],而后由Butler在Rodin 平臺上實現為Theory 插件[59],并提供了Array、Stack、Sequence、Tree、B-Tree 等一系列的標準抽象數據類型庫.建模人員既可以根據需要定義自己所需要的新的抽象數據類型,也可以直接使用Rodin 中的標準庫.由于抽象數據類型也可以被視為一種可重用的模式,Basin 等將Theory 方法和Generic Instantiation 方法結合起來[60],使其能夠應用于大型復雜系統的形式化建模及驗證.Fürst和Hoang用這種綜合性的方法構造了復雜的列控系統的形式化模型[61,62],證明了該方法能夠減少手工證明的工作量.

Event-B 抽象數據類型的優勢在于它能夠大幅提升自動定理證明的程度,而傳統的基于精化的方式則需要大量手動證明.而其局限性在于,它沒有提供參數化的抽象數據類型的Event-B 模型,即通用的抽象數據類型(例如,一個與元素類型無關的通用的堆棧類型).因此,在實際使用時還無法像面向對象語言的模板類那樣通用.

對各種可重用的Event-B 模型的總結如表2所示.

表2 可重用的Event-B 模型方法總結

2.4 實時Event-B 模型

實時并發系統的復雜性使得其驗證過程必須使用形式化方法來完成,它使得研究人員能夠使用嚴格的數學模型來描述系統的需求以及系統的行為,并驗證給定的系統或系統模型是否滿足所要求的行為屬性.然而,Event-B 本身不支持建模時間概念,在表達時間方面的能力有一定的局限,因此也難以完成實時系統的時間屬性的驗證.

為解決Event-B對實時系統的建模問題,研究人員已經做了一些前期的工作.其主要方法是使用Event-B 建模語言本身的能力來建模時間,通常是使用離散的時鐘滴答事件(tick_tock)來建模時間的流逝,并建模各種時間間隔模式;Butler 等[63]最早提出了在經典B 中建模離散時間的方法,這種方法使用一個自然數變量(名叫時鐘變量)來表達當前時間,通過增加這個變量的值來表示時間的流逝.他和經典的時間系統的最大區別在于,如果當前時間等于截止時間,則使用一定的操作來阻止時間的流逝.這種建模思想被后續的所有工作所采納.是后續所有實時Event-B 模型的理論基礎.

Cansell 等[64]首先提出了Event-B的時間約束模式的概念,并專門采用tick_tock 事件來表達時間的流逝.時間約束模式首先將時間的流逝與Event-B 中的事件關聯起來,并將事件發生的次序從定性的“先后次序”精確到了用變量表達的時間段上.但是Cansell 并沒有進一步對各種時間模式進行分類.

Rehm 等[65-67]提出了“持續時間模式”(duration pattern)來表達一個事件的持續時間,讓建模人員可以在Event-B 框架中對實時屬性進行建模和推理.但是同樣沒有對各種時間模式分類.

Sarshogha 等[68,69]提出了3 種時間模式:Delay 模式、Expiry 模式和Deadline 模式,用來表示實時系統的延遲、超時和截止期的概念.這3 種模式的提出,為實時系統的Event-B 建模提供了通用的參考模型.但是其模式沒有考慮時間間隔問題,且模式所考慮的場景較少.

Sulskus 等[70,71]在Sarshogha的工作基礎上提出了時間間隔方法,用iUML-B 狀態機的單個狀態表示時間間隔,并分別用狀態節點的入邊和出邊來表示該時間間隔的觸發事件(trigger)和響應事件(response).Sulskus開發了一個稱為tiGen (time interval Generator)的工具來支持其時間建模的思想.

時間間隔方法的優勢在于其使用JSD 風格和iUMLB 狀態機共同表達了各種時間間隔模式,為實時系統的形式化建模及正確性證明提供了豐富的可重用的實時模式,并節省了大量的時間屬性的證明工作.這種方法的局限在于,它依然是在Event-B 建模框架中描述實時系統,仍然需要大量的手工證明工作.另外,這些模式也無法方便地轉換為時間轉換系統模型,因此也難以使用模型檢測方法來減輕時間屬性驗證的負擔.

在表3中對各種實時Event-B 建模方法的優缺點做出了總結.

表3 實時Event-B 方法總結

2.5 國內外研究現狀小結

可以看出,自從Event-B 建模方法被提出以來,研究人員已經提出了大量的新方法、新思路和支持工具來幫助其支持軟件開發過程.經過近十幾年的努力,這些方法及其所提出的插件被集成到基于Eclipse 開發的Rodin 平臺上,存在很好的互操作性.表4總結了近年來Event-B為支持軟件工程和系統工程的全壽命周期所提出的方法和插件.

表4 Event-B為支持軟件工程和系統工程所提出的方法和插件

3 發展的挑戰和方向

3.1 挑戰

(1)隨著“軟件定義”時代的到來,軟件的應用領域已擴充到人類認識所能達到的所有領域,軟件的范型已經從結構化、構件化范型變為服務化、網絡化、云化范型.軟件范型的轉變必然對軟件工程形式化方法帶來新的挑戰.這種挑戰對基于Event-B的“構造即正確”的方法尤為明顯.系統正確性的關注點已不再局限于某個模塊、組件內部的正確性,還需要考慮系統整體的大量的對象交互、行為互操作等特點.

(2)軟件的規模、復雜性呈現爆炸式增長,傳統的模型檢測方法因其探索空間有限,無法完成大型復雜軟件系統的各種行為屬性驗證.而基于Event-B的形式化方法也面臨著證明工作繁雜、證明效率低等問題.

(3)軟件制造的泛在化對軟件形式化建模工具提出了更多的易用性、易理解性的要求,也為軟件工程形式化提出了更多的挑戰.大量的非計算機專業的系統開發人員需要更加貼近用戶需求的非形式化的“前端”來描述問題域、進行需求分析,并能在工具的支持下將這些非形式化的領域模型轉換為Event-B 模型.

3.2 發展的方向

對于以上挑戰,本文提出以下幾點應對方案,也是對未來基于Event-B的軟件工程形式化方法的趨勢的預測:

(1)增加對軟件體系結構建模工具的支持,讓其能夠表達大粒度的系統構件之間的控制流和數據流關系并映射為Event-B 模型.這種方法使系統構建者能夠從更加宏觀和抽象的視角研究系統的“涌現”特性,而不是關注于某些方面的實現細節的正確性.現有的對Event-B和BIP[75]共同進行組合建模的工作以及將SysML[76,77]和UML 活動圖[78]轉換為Event-B 模型的工作是一個很好解決方案,de Sousa和Snook 等提出了將IOD 也歸入到UML-B 中的建議[79]也能讓Event-B更加符合軟件工程人員的習慣,但是還缺少在Rodin環境中的工具支持.

(2)增加對新的編程范型的半形式化建模工具的支持以及這些建模工具到Event-B 語言的轉換工具.在這些領域,研究人員正在開展的工作包括使用Event-B 建立面向服務的架構[80]、微服務架構[81]、云計算[82]、物聯網應用[83]、區塊鏈[84]、自適應軟件[85]等,但所提出的方法還沒有形成系統的、可用的插件和工具.

(3)提出更多的、更加適合最終用戶的領域編程語言和領域建模工具以及相應的模型轉換工具,實現各種非形式化的領域建模語言到Event-B 模型的轉換,為問題域到解空間的映射提供更好的橋梁.由法國國家研究局ANR 支持的IMPEX 工程正在研究如何將本體語言描述的領域本體模型轉換為Event-B的本體結構[86,87],是一個可以參考的方案.

(4)通用軟件的安全性和可靠性需求會催生更多將Event-B 模型轉換為行為模型的模型轉換工具.Event-B沒有行為語義,也沒有時間語義,這也使得我們可以將其映射到任何所需的論域,例如Labeled Transition System[88]及其各種變體,如Timed Transition system[89]等,為其賦予行為語義和時間語義,從而完成各種行為屬性和時間屬性的驗證.Peng 等[90]在Event-B的LTS語義方面所做的研究可以作為一個參考的思路.

4 結束語

當前計算的泛在化趨勢、信息系統向物理世界遷移以及人機物融合的趨勢將形式化方法的應用從安全關鍵領域滲透到各種通用軟件領域,對各種新方法、新工具以及集成開發環境的要求日益迫切.Event-B 作為一種支持“correct-by-construction”思想的定理證明語言,為軟件工程形式化提供了重要支撐.

本文首次以軟件工程對形式化方法所提出的需求為出發點,以一種形式化建模語言對軟件工程全壽命周期的支持程度來研究軟件工程形式化方法,對Event-B 建模語言為軟件工程所提供的支撐進行分類闡述,對軟件工程形式化方法的推廣和應用具有一定的借鑒和參考價值.