摘 要

傳統(tǒng)的軟件架構(gòu)設(shè)計(jì)一般采用非形式化的方法，通過各類圖表從不同角度對(duì)系統(tǒng)進(jìn)行描述，這種架構(gòu)設(shè)計(jì)方式依賴設(shè)計(jì)者的經(jīng)驗(yàn)知識(shí)，無法保證設(shè)計(jì)質(zhì)量。本文將形式化建模引入架構(gòu)設(shè)計(jì)，通過嚴(yán)格的形式化定義描述系統(tǒng)運(yùn)行過程及需求約束，在保證模型正確的基礎(chǔ)上導(dǎo)出架構(gòu)設(shè)計(jì)，從而保證架構(gòu)設(shè)計(jì)質(zhì)量。

【關(guān)鍵詞】Event-B 形式化建模 軟件架構(gòu) 動(dòng)態(tài)車載導(dǎo)航系統(tǒng)

1 引言

動(dòng)態(tài)車載導(dǎo)航系統(tǒng)是一個(gè)大型分布式系統(tǒng)，且是一個(gè)軟件密集型系統(tǒng)。在這個(gè)系統(tǒng)中，物理實(shí)體包括車載終端、車載網(wǎng)關(guān)、基站、Wi-Fi接入點(diǎn)以及交通信息中心的服務(wù)端網(wǎng)關(guān)/代理和各服務(wù)節(jié)點(diǎn)。如何進(jìn)行系統(tǒng)的功能模塊劃分以及各功能模塊之間如何通信，這些都是系統(tǒng)架構(gòu)設(shè)計(jì)將要回答的問題。

最常見的架構(gòu)設(shè)計(jì)方法是使用各種圖表從不同角度對(duì)系統(tǒng)進(jìn)行描述，如使用“4+1”視圖或其該進(jìn)版本。使用圖表能夠形象地刻畫軟件系統(tǒng)的結(jié)構(gòu)，各組件間的交互。但是，這種方法有一個(gè)問題：它是一種非形式化方法，無法量化評(píng)價(jià)，因此無法精確判斷架構(gòu)設(shè)計(jì)的正確性。為此，人們提出了使用形式化方法對(duì)系統(tǒng)進(jìn)行建模，然后通過形式化模型導(dǎo)出架構(gòu)設(shè)計(jì)，這也正是本文所采用的架構(gòu)設(shè)計(jì)方法。本文將基于Event-B這一形式化建模方法對(duì)車載導(dǎo)航系統(tǒng)建模。

Event-B最早由Abrial教授于2003年的兩篇論文中提及，可以用于復(fù)雜系統(tǒng)建模。Event-B自出現(xiàn)以來便受到了廣泛關(guān)注，相關(guān)研究從未停止，如應(yīng)用Event-B對(duì)網(wǎng)絡(luò)協(xié)議建模、應(yīng)用Event-B 進(jìn)行并發(fā)編程以及應(yīng)用Event-B開發(fā)衛(wèi)星軟件等。由于Event-B是一種形式化建模方法，整個(gè)模型均是使用嚴(yán)格的數(shù)學(xué)語言進(jìn)行描述，因此可以量化分析，并可通過自動(dòng)化的軟件工具進(jìn)行輔助建模，如Rodin平臺(tái)，它可以實(shí)現(xiàn)自動(dòng)的推理規(guī)則證明，從而提高建模效率。

2 動(dòng)態(tài)車載導(dǎo)航系統(tǒng)模型

2.1 需求

本節(jié)將應(yīng)用Event-B對(duì)動(dòng)態(tài)車載導(dǎo)航系統(tǒng)建模，這是一個(gè)反復(fù)迭代的過程。從初始模型開始，不斷對(duì)其精化，直到模型滿足要求為止。

首先，我們得確定系統(tǒng)需求。從目前市面上普遍使用的車載導(dǎo)航系統(tǒng)出發(fā)，可以得出車載導(dǎo)航系統(tǒng)應(yīng)具有的基本功能：地圖顯示、導(dǎo)航和路線規(guī)劃。為了方便后續(xù)分析設(shè)計(jì)，我們將以一種規(guī)范的形式描述需求：每個(gè)需求除了有文字描述之外，還必須對(duì)其進(jìn)行標(biāo)記，以方便后續(xù)引用。

針對(duì)上述基本功能，可以得到如表1需求描述。

除了上述3項(xiàng)基本功能外，由于動(dòng)態(tài)車載導(dǎo)航系統(tǒng)特殊的系統(tǒng)結(jié)構(gòu)：系統(tǒng)可分為客戶端子系統(tǒng)（主要運(yùn)行于車載終端）和服務(wù)端子系統(tǒng)（主要運(yùn)行于各服務(wù)節(jié)點(diǎn)）。則客戶端子系統(tǒng)的需求如表2所示。

服務(wù)端子系統(tǒng)的需求如表3所示。

2.2 精化策略

精化策略是建模前需要考慮的建模步驟。建模過程是按步驟向前推進(jìn)的，每一步會(huì)輸出一個(gè)模型，后一個(gè)模型總是比前一個(gè)模型更詳細(xì)，更完善。

思考精化策略可以從需求出發(fā)，對(duì)需求排序，然后確定每一步模型需要滿足的需求。在對(duì)系統(tǒng)需求排序之后，可以形成如下精化策略：

（1）初始模型將只考慮需求E-1和E-4，實(shí)現(xiàn)動(dòng)態(tài)導(dǎo)航系統(tǒng)的地圖傳輸功能；

（2）下一步將引入地圖顯示功能（需求F-1）。此時(shí)，我們實(shí)現(xiàn)了導(dǎo)航系統(tǒng)的第一個(gè)基本功能；

（3）然后，將考慮需求E-2、F-4和E-5，實(shí)現(xiàn)導(dǎo)航系統(tǒng)的路網(wǎng)傳輸和地圖匹配功能；

（4）在下一次精化，將完善客戶端地圖匹配與地圖顯示之間的操作流程，為后續(xù)實(shí)現(xiàn)導(dǎo)航和路線規(guī)劃做好準(zhǔn)備；

（5）最后一次精化，將實(shí)現(xiàn)需求E-3、F-5和E-6，從而最終實(shí)現(xiàn)F-2（導(dǎo)航）和F-3（路線規(guī)劃）。至此，實(shí)現(xiàn)了導(dǎo)航系統(tǒng)的三大基本功能。

2.3 建模

為了更好地描述初始模型，不妨假設(shè)車載終端為客戶端，它與服務(wù)端之間構(gòu)成了一個(gè)C/S結(jié)構(gòu)，客戶端和服務(wù)端將被抽象成模型的兩個(gè)機(jī)器（Machine）。它們之間的數(shù)據(jù)傳輸如圖1所示。

之后，我們可以為每個(gè)Machine定義上下文：集合、常量和公理，通過這些元素可以定義映射：在Machine的事件中可用于表達(dá)函數(shù)。

Event-B建模的重點(diǎn)是定義事件，它負(fù)責(zé)改變Machine的狀態(tài)，從而實(shí)現(xiàn)相應(yīng)的系統(tǒng)功能。為此，我們還需要定義變量、不變式（變量應(yīng)滿足的條件），并將系統(tǒng)功能描述為一系列執(zhí)行步驟，然后為每一步定義一個(gè)事件，從而完成建模。

最終，我們可以將模型輸入Rodin平臺(tái)，利用其自動(dòng)證明功能來完成模型驗(yàn)證。對(duì)于本文的導(dǎo)航系統(tǒng)，我們定義了5個(gè)模型，分別對(duì)應(yīng)精化策略的5個(gè)步驟。這5個(gè)模型在Rodin平臺(tái)共生成了69條證明義務(wù)，并全部自動(dòng)證明成功。因此，我們可以得出結(jié)論：這些模型在理論上是正確的。這也間接驗(yàn)證了導(dǎo)航系統(tǒng)架構(gòu)的正確性。

3 總結(jié)

本文分析了動(dòng)態(tài)車載導(dǎo)航系統(tǒng)的主要需求，但并未在需求分析之后直接開始軟件架構(gòu)設(shè)計(jì)，而是在架構(gòu)設(shè)計(jì)之前進(jìn)行系統(tǒng)建模，這看似增加了系統(tǒng)開發(fā)的工作量，但由于使用的建模方式是形式化建模，可以借助相關(guān)數(shù)學(xué)理論對(duì)模型進(jìn)行驗(yàn)證，修正模型中的錯(cuò)誤，直至最終構(gòu)建出正確的模型。這實(shí)際上是將傳統(tǒng)軟件開發(fā)只能在編碼階段進(jìn)行的調(diào)試工作提前到架構(gòu)設(shè)計(jì)之前，能提早發(fā)現(xiàn)并修改錯(cuò)誤，在一定程度上避免了重大設(shè)計(jì)缺陷在編碼階段才暴露的問題，因而，這種架構(gòu)設(shè)計(jì)方法節(jié)約了開發(fā)與維護(hù)的成本，提高了系統(tǒng)開發(fā)效率。

參考文獻(xiàn)

[1]P.B.Kruchten，“The 4+1 View Model of architecture，”Software，IEEE，1995，12（06）：42-50.

[2]M.Che and D.E.Perry，“Scenario-Based Architectural Design Decisions Documentation and Evolution，” in Engineering of Computer Based Systems （ECBS），2011：216–225.

[3]J.-R.Abrial，“B#： Toward a Synthesis between Z and B，”in ZB 2003：Formal Specification and Development in Z and B，vol.2651， 2003：168–177.

[4]J.-R.Abrial，“Event Based Sequential Program Development：Application to Constructing a Pointer Program，”in FME 2003：Formal Methods，vol.2805，2003：51–74.

[5]X.-J.Wang and H.Zhang，“Modeling of TCP Protocol in Event-B，”in INFORMATION TECHNOLOGY APPLICATIONS IN INDUSTRY，PTS 1-4，2013：1156–1159.

[6]T.Hoang and J.-R.Abrial，“Event-B Decomposition for Parallel Programs，”in Abstract State Machines，Alloy，B and Z，vol.5977， 2010：319–333.

[7]A.Iliasov，E.Troubitsyna，L. Laibinis，A.Romanovsky，K. Varpaaniemi，D.Ilic，and T. Latvala，“Developing mode-rich satellite software by refinement in Event-B，”SCIENCE OF COMPUTER PROGRAMMING，2013：884–905.

[8]J.-R.Abrial，M.Butler，S.Hallerstede，T.Hoang，F(xiàn).Mehta，and L.Voisin，“Rodin： an open toolset for modelling and reasoning in Event-B，”International Journal on Software Tools for Technology Transfer，2010：447-466.

作者簡(jiǎn)介

祁暉（1983-），男，福建省莆田市人。研究生學(xué)歷，博士學(xué)位。現(xiàn)為長(zhǎng)春理工大學(xué)計(jì)算機(jī)科學(xué)技術(shù)學(xué)院講師。主要研究方向?yàn)橛?jì)算機(jī)網(wǎng)絡(luò)與網(wǎng)絡(luò)安全。

作者單位

長(zhǎng)春理工大學(xué)計(jì)算機(jī)科學(xué)技術(shù)學(xué)院 吉林省長(zhǎng)春市 130022