本书首先分析了动态车载导航系统的核心需求:地图显示、导航和路线规划,然后运用Event-B形式化建模方法对系统进行建模分析。在模型精化过程中,论述了相关数据结构及流程的建模方法。模型经过4次精化,实现了所有的核心需求。将每个精化模型导入Rodin平台,所生成的证明义务全部证明成功,表明该模型在理论上是正确的。之后以模型为参考,设计了导航系统的软件架构,从逻辑视图和过程视图两个角度对系统进行非形式化描述,系统开发人员可在该架构的基础上设计并开发出正确的系统。第3章到第6章,我们重点研究了动态车载导航系统的访问控制技术、地图缓存技术、地图匹配技术和智能信息处理技术。
移动互联网的发展使得车载导航系统从静态自主式转向动态协作式。原有封闭独立的体系结构被打破,取而代之的将是一种更加开放的体系结构。同时,大量便携式智能终端设备的涌现使得导航系统不仅能运行在车载终端上,也能运行在智能手机、平板电脑等支持互联网接入的智能终端上。导航系统正逐渐演变成一种用户可以随时随地使用的服务。这些变化将给导航系统研发带来更多的技术挑战,从系统架构设计到一些关键技术实现以及应用模式,都将做出适当调整以解决新的问题。《车载通信与动态导航系统》围绕动态车载导航系统的一个架构和三个核心关键技术展开论述。架构总领整个导航系统的设计与开发,三个核心关键技术是架构中的重要组成部分。《车载通信与动态导航系统》向读者展示了这些关键技术是如何解决系统研发过程中遇到的难题,为从事或希望从事相关领域研发的科研人员或开发者提供有益参考。