移动互联网的发展使得车载导航系统从静态自主式转向动态协作式。原有封闭独立的体系结构被打破，取而代之的是一种更加开放的体系结构。同时，大量便携式智能终端设备的涌现使得导航系统不仅能运行在车载终端上，也能运行在智能手机、平板电脑等支持互联网接入的智能终端上。导航系统正逐渐演变成一种用户可以随时随地使用的服务。这些变化将给导航系统带来更多的技术挑战，从系统架构设计到一些关键技术实现以及应用模式，都需要做出适当调整以解决新的问题。本文首先分析了动态车载导航系统的核心需求：地图显示、导航和路线规划，然后运用Event-B形式化建模方法对系统进行建模分析。在模型精化过程中，论述了相关数据结构及流程的建模方法。模型经过4次精化，实现了所有的核心需求。将每个精化模型导入Rodin平台，所生成的证明义务全部证明成功，表明该模型在理论上是正确的。之后以模型为参考，设计了导航系统的软件架构，从逻辑视图和过程视图两个角度对系统进行非形式化描述，系统开发人员可在该架构的基础上设计并开发出正确的系统。接下来，本文重点研究了动态车载导航系统的地图缓存技术、地图匹配技术和智能信息处理技术。关于地图缓存技术，本文为动态车载导航系统设计并实现了一种基于二级地图分块的缓存系统。该系统包含索引文件、数据文件及相关程序。对缓存系统的索引文件结构、数据文件结构以及专门针对稀疏矩阵的高速缓存结构进行了详细设计，并在这些数据结构的基础上形成了管理缓存的有效策略。实验结果表明该缓存系统对于加快动态车载导航系统的响应速度，减少网络传输数据量具有良好作用。本文还研究了缓存预取策略，该策略通过分析车辆行驶前方的路网和路口模式来预测车辆的行驶轨迹，将此预测结果与启发式预取策略的预测结果相结合，从而得到更准确的预测结果。实验表明，该缓存预取策略进一步改善了启发式预取策略的性能，有效减少了系统所需的地图分块数量。关于地图匹配技术，本文分析了各种地图匹配算法，确定了影响地图匹配性能的关键是路口匹配，并对路口匹配问题做了深入研究，提出了路口决策域模型。该模型主要参考与路口相连的路段宽度、路段夹角、车载GPS精度以及路网数据精度等信息。本文利用此模型对基于隐马尔科夫模型（HMM）的地图匹配算法做了改进。实验结果表明，改进后的匹配算法能够有效降低路口匹配错误率，提高导航系统导航的稳定性。此外，为了解决延迟匹配问题，本文分析了车辆的转向特征，设计了车辆转向识别方法，并利用该方法改进了基于路口决策域模型的地图匹配算法，缩短了匹配点停止于路口的时间。关于智能信息处理技术，本文应用机器学习技术对车辆转向识别方法做了改进。探索了两种建立车辆转向识别模型的学习方法：第一种方法首先应用改进的K-means算法对训练数据进行快速聚类，然后应用SVM算法建立识别模型，最后应用F-measure方法评价模型的识别性能并选择最优的模型；第二种方法应用基于多维高斯分布的异常检测算法建立识别模型，之后应用F-measure方法确定模型参数。实验结果表明应用这两种方法构建的车辆转向识别模型均具备较好的泛化能力。基于以上研究成果，本文设计并实现了基于动态导航系统的车辆转向识别学习系统，并将此系统应用于基于路口决策域模型的地图匹配算法，在一定程度上解决了延迟匹配问题。