基于Event-B的动态车载导航系统架构设计

传统的软件架构设计一般采用非形式化的方法,通过各类图表从不同角度对系统进行描述,这种架构设计方式依赖设计者的经验知识,无法保证设计质量。本文将形式化建模引入架构设计,通过严格的形式化定义描述系统运行过程及需求约束,在保证模型正确的基础上导出架构设计,从而保证架构设计质量。