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

1(西安航空學(xué)院 計(jì)算機(jī)學(xué)院,西安 710077)

2(西安石油大學(xué) 計(jì)算機(jī)學(xué)院,西安 710065)

1 引言

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

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

本文首先對(duì)已有的基于Event-B的軟件工程形式化方法進(jìn)行了分類闡述,主要分為Event-B 模型的控制結(jié)構(gòu)、面向?qū)ο蟮腅vent-B 模型、可重用的Event-B 模型、實(shí)時(shí)Event-B 模型.而后對(duì)基于Event-B的軟件工程形式化方法的未來發(fā)展方向提出了預(yù)測和建議;最后對(duì)本文內(nèi)容進(jìn)行總結(jié).

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

2.1 Event-B 模型的控制結(jié)構(gòu)

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

(1)邊精化和節(jié)點(diǎn)精化

為了能夠清晰地表達(dá)Event-B 模型的事件次序,Hallerstede 等介紹了一套結(jié)構(gòu)化的符號(hào)來描述Event-B 模型的3 種基本結(jié)構(gòu)(step,loop,choice)[4]和1 種復(fù)合結(jié)構(gòu)box.在其符號(hào)系統(tǒng)中,采用斷言作為節(jié)點(diǎn),并用事件在轉(zhuǎn)換邊上標(biāo)記.采用這種方法,能夠讓Event-B 模型中的事件次序變得更加清晰,同時(shí)也能夠讓不變式變得更加簡單.在此基礎(chǔ)上,Hallerstede 等在文獻(xiàn)[5]中提出了對(duì)狀態(tài)轉(zhuǎn)換系統(tǒng)進(jìn)行精化的兩種方法:邊精化和節(jié)點(diǎn)精化.從Event-B 模型的角度來說,邊精化就是對(duì)事件的分解,將一個(gè)事件分解為幾個(gè)子事件;而節(jié)點(diǎn)精化則是對(duì)狀態(tài)的精化,是將一個(gè)抽象狀態(tài)精化為幾個(gè)具體的狀態(tài).

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

(2)事件精化結(jié)構(gòu)

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

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

Fathabadi 等持續(xù)改進(jìn)AD 方法,并將其重新命名為ERS (Event Refinement Structure)方法[12],將AD 插件做了進(jìn)一步的完善,變?yōu)镋RS 插件.

事件精化結(jié)構(gòu)的優(yōu)勢在于,系統(tǒng)建模人員可以從宏觀上評(píng)估各種精化結(jié)構(gòu)的優(yōu)劣,為評(píng)估不同的系統(tǒng)精化策略提供依據(jù).同時(shí)AD/ERS 圖形化插件所表達(dá)的事件精化結(jié)構(gòu)可以生成大部分的Event-B 控制流代碼,免除了建模人員的手工編碼負(fù)擔(dān).

事件精化結(jié)構(gòu)的局限在于,它更適合表達(dá)各精化層級(jí)之間的靜態(tài)的精化關(guān)系,也就是事件精化的靜態(tài)結(jié)構(gòu).在表達(dá)系統(tǒng)的動(dòng)態(tài)行為方面,AD/ERS 方法所使用的樹形結(jié)構(gòu)圖并不直觀.AD/ERS 方法的另一個(gè)局限就是很難映射到類似CSP 或者LTS 這樣的行為語義模型上,因此也就難以方便的驗(yàn)證模型的行為屬性.

(3)流語言

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

流語言的優(yōu)勢在于,它能直接用平面的圖形來表達(dá)事件之間的觸發(fā)-響應(yīng)關(guān)系,也就是事件的發(fā)生次序,從這個(gè)角度來說,它比AD/ERS 方法更好.同時(shí)它也提供了并發(fā)事件和互斥事件的表達(dá)方式,對(duì)并發(fā)程序的建模提供了支持.

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

(4)CSP||B

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

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

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

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

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

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

Event-B對(duì)控制結(jié)構(gòu)提供支持的方法的總結(jié)如表1所示.

表1 Event-B 模型的控制結(jié)構(gòu)方法總結(jié)

2.2 面向?qū)ο蟮腅vent-B

面向?qū)ο蠓椒ㄒ恢笔墙Y(jié)構(gòu)化設(shè)計(jì)和增強(qiáng)軟件模塊內(nèi)聚性的公認(rèn)的方法,用于體現(xiàn)面向?qū)ο蟮南到y(tǒng)分析與設(shè)計(jì)思想的統(tǒng)一建模語言UML 也已被廣大工程人員所接受.Event-B的研究人員為推進(jìn)Event-B在工程方面的應(yīng)用,提出了一系列的綜合UML和Event-B的方法,為Event-B 模型的結(jié)構(gòu)化做出了貢獻(xiàn).

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

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

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

UML-B的局限性包括:首先,類圖和狀態(tài)圖的粒度過細(xì),對(duì)于復(fù)雜系統(tǒng)來說,會(huì)有過多的交互和控制流需要表達(dá).其次,UML-B 模型無法與已有的Event-B machine 集成;最后,UML-B 狀態(tài)機(jī)表達(dá)方式無法表達(dá)并行的狀態(tài)機(jī).

為解決UML-B的缺點(diǎn),南安普頓大學(xué)對(duì)UMLB 持續(xù)地改進(jìn),使之能夠嵌入到傳統(tǒng)的Event-B 模型代碼中,并將現(xiàn)存的Event-B 模型中的事件與狀態(tài)機(jī)中的事件“鏈接”起來,從而達(dá)到控制事件次序的效果.目前,UML-B 已經(jīng)發(fā)展為“集成的UML-B”(integrated UML-B,iUML-B),并已應(yīng)用于各領(lǐng)域的系統(tǒng)建模[38].iUML-B 狀態(tài)機(jī)的另一個(gè)重要的優(yōu)勢就是引入了并發(fā)狀態(tài)機(jī),為直觀地建模并發(fā)系統(tǒng)提供了支持.

2.3 可重用的Event-B 模型

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

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

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

基于接口的Event-B 模型的優(yōu)勢是分離了Event-B模型的接口描述和接口實(shí)現(xiàn),達(dá)到了形式化模型的接口與實(shí)現(xiàn)分離.由此而帶來的好處包括:支持Event-B模型的架構(gòu)設(shè)計(jì)和推理;各模塊的實(shí)現(xiàn)可以獨(dú)立完成,而不用關(guān)注其他模塊的變化;提升了Event-B 模型的可擴(kuò)展性等.同時(shí),基于接口的Event-B 模型也解決了多層、多模態(tài)的控制系統(tǒng)中模式一致性難以驗(yàn)證的問題,并利用架構(gòu)分解的方法降低了大型復(fù)雜系統(tǒng)的形式化模型的復(fù)雜度.

基于接口的Event-B 模型的局限性在于,它對(duì)形式化模型的設(shè)計(jì)者的經(jīng)驗(yàn)有著更高的要求.接口一旦定義,就無法在后續(xù)的過程中隨意修改.因?yàn)楹罄m(xù)的精化都必須符合接口的需求.這從某種程度上限制了形式化模型的設(shè)計(jì)者對(duì)設(shè)計(jì)空間的探索.

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

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

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

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

(3)Event-B 設(shè)計(jì)模式

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

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

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

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

Event-B 抽象數(shù)據(jù)類型的優(yōu)勢在于它能夠大幅提升自動(dòng)定理證明的程度,而傳統(tǒng)的基于精化的方式則需要大量手動(dòng)證明.而其局限性在于,它沒有提供參數(shù)化的抽象數(shù)據(jù)類型的Event-B 模型,即通用的抽象數(shù)據(jù)類型(例如,一個(gè)與元素類型無關(guān)的通用的堆棧類型).因此,在實(shí)際使用時(shí)還無法像面向?qū)ο笳Z言的模板類那樣通用.

對(duì)各種可重用的Event-B 模型的總結(jié)如表2所示.

表2 可重用的Event-B 模型方法總結(jié)

2.4 實(shí)時(shí)Event-B 模型

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

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

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

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

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

Sulskus 等[70,71]在Sarshogha的工作基礎(chǔ)上提出了時(shí)間間隔方法,用iUML-B 狀態(tài)機(jī)的單個(gè)狀態(tài)表示時(shí)間間隔,并分別用狀態(tài)節(jié)點(diǎn)的入邊和出邊來表示該時(shí)間間隔的觸發(fā)事件(trigger)和響應(yīng)事件(response).Sulskus開發(fā)了一個(gè)稱為tiGen (time interval Generator)的工具來支持其時(shí)間建模的思想.

時(shí)間間隔方法的優(yōu)勢在于其使用JSD 風(fēng)格和iUMLB 狀態(tài)機(jī)共同表達(dá)了各種時(shí)間間隔模式,為實(shí)時(shí)系統(tǒng)的形式化建模及正確性證明提供了豐富的可重用的實(shí)時(shí)模式,并節(jié)省了大量的時(shí)間屬性的證明工作.這種方法的局限在于,它依然是在Event-B 建?？蚣苤忻枋鰧?shí)時(shí)系統(tǒng),仍然需要大量的手工證明工作.另外,這些模式也無法方便地轉(zhuǎn)換為時(shí)間轉(zhuǎn)換系統(tǒng)模型,因此也難以使用模型檢測方法來減輕時(shí)間屬性驗(yàn)證的負(fù)擔(dān).

在表3中對(duì)各種實(shí)時(shí)Event-B 建模方法的優(yōu)缺點(diǎn)做出了總結(jié).

表3 實(shí)時(shí)Event-B 方法總結(jié)

2.5 國內(nèi)外研究現(xiàn)狀小結(jié)

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

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

3 發(fā)展的挑戰(zhàn)和方向

3.1 挑戰(zhàn)

(1)隨著“軟件定義”時(shí)代的到來,軟件的應(yīng)用領(lǐng)域已擴(kuò)充到人類認(rèn)識(shí)所能達(dá)到的所有領(lǐng)域,軟件的范型已經(jīng)從結(jié)構(gòu)化、構(gòu)件化范型變?yōu)榉?wù)化、網(wǎng)絡(luò)化、云化范型.軟件范型的轉(zhuǎn)變必然對(duì)軟件工程形式化方法帶來新的挑戰(zhàn).這種挑戰(zhàn)對(duì)基于Event-B的“構(gòu)造即正確”的方法尤為明顯.系統(tǒng)正確性的關(guān)注點(diǎn)已不再局限于某個(gè)模塊、組件內(nèi)部的正確性,還需要考慮系統(tǒng)整體的大量的對(duì)象交互、行為互操作等特點(diǎn).

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

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

3.2 發(fā)展的方向

對(duì)于以上挑戰(zhàn),本文提出以下幾點(diǎn)應(yīng)對(duì)方案,也是對(duì)未來基于Event-B的軟件工程形式化方法的趨勢的預(yù)測:

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

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

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

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

4 結(jié)束語

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

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