基于Event—B的動態車載導航系統架構設計

摘 要

傳統的軟件架構設計一般采用非形式化的方法，通過各類圖表從不同角度對系統進行描述，這種架構設計方式依賴設計者的經驗知識，無法保證設計質量。本文將形式化建模引入架構設計，通過嚴格的形式化定義描述系統運行過程及需求約束，在保證模型正確的基礎上導出架構設計，從而保證架構設計質量。

【關鍵詞】Event-B 形式化建模 軟件架構 動態車載導航系統

1 引言

動態車載導航系統是一個大型分布式系統，且是一個軟件密集型系統。在這個系統中，物理實體包括車載終端、車載網關、基站、Wi-Fi接入點以及交通信息中心的服務端網關/代理和各服務節點。如何進行系統的功能模塊劃分以及各功能模塊之間如何通信，這些都是系統架構設計將要回答的問題。

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

Event-B最早由Abrial教授于2003年的兩篇論文中提及，可以用于復雜系統建模。Event-B自出現以來便受到了廣泛關注，相關研究從未停止，如應用Event-B對網絡協議建模、應用Event-B 進行并發編程以及應用Event-B開發衛星軟件等。由于Event-B是一種形式化建模方法，整個模型均是使用嚴格的數學語言進行描述，因此可以量化分析，并可通過自動化的軟件工具進行輔助建模，如Rodin平臺，它可以實現自動的推理規則證明，從而提高建模效率。

2 動態車載導航系統模型

2.1 需求

本節將應用Event-B對動態車載導航系統建模，這是一個反復迭代的過程。從初始模型開始，不斷對其精化，直到模型滿足要求為止。

首先，我們得確定系統需求。從目前市面上普遍使用的車載導航系統出發，可以得出車載導航系統應具有的基本功能：地圖顯示、導航和路線規劃。為了方便后續分析設計，我們將以一種規范的形式描述需求：每個需求除了有文字描述之外，還必須對其進行標記，以方便后續引用。

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

除了上述3項基本功能外，由于動態車載導航系統特殊的系統結構：系統可分為客戶端子系統（主要運行于車載終端）和服務端子系統（主要運行于各服務節點）。則客戶端子系統的需求如表2所示。

服務端子系統的需求如表3所示。

2.2 精化策略

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

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

（1）初始模型將只考慮需求E-1和E-4，實現動態導航系統的地圖傳輸功能；

（2）下一步將引入地圖顯示功能（需求F-1）。此時，我們實現了導航系統的第一個基本功能；

（3）然后，將考慮需求E-2、F-4和E-5，實現導航系統的路網傳輸和地圖匹配功能；

（4）在下一次精化，將完善客戶端地圖匹配與地圖顯示之間的操作流程，為后續實現導航和路線規劃做好準備；

（5）最后一次精化，將實現需求E-3、F-5和E-6，從而最終實現F-2（導航）和F-3（路線規劃）。至此，實現了導航系統的三大基本功能。

2.3 建模

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

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

Event-B建模的重點是定義事件，它負責改變Machine的狀態，從而實現相應的系統功能。為此，我們還需要定義變量、不變式（變量應滿足的條件），并將系統功能描述為一系列執行步驟，然后為每一步定義一個事件，從而完成建模。

最終，我們可以將模型輸入Rodin平臺，利用其自動證明功能來完成模型驗證。對于本文的導航系統，我們定義了5個模型，分別對應精化策略的5個步驟。這5個模型在Rodin平臺共生成了69條證明義務，并全部自動證明成功。因此，我們可以得出結論：這些模型在理論上是正確的。這也間接驗證了導航系統架構的正確性。

3 總結

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

參考文獻

[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.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.

作者簡介

祁暉（1983-），男，福建省莆田市人。研究生學歷，博士學位。現為長春理工大學計算機科學技術學院講師。主要研究方向為計算機網絡與網絡安全。

作者單位

長春理工大學計算機科學技術學院 吉林省長春市 130022