基于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