形式化开发过程 ·建立需求与系统模型之间的映射关系 -模型获取 Requirement △△△ ·从现实世界向模型表示的转化过程 capture ·形式规约 System 一模型验证 modelling ·判断模型表示是否符合需求 System ·形式证明与验证 synthesis -模型变换 ·从模型表示向计算机系统的转化过程 一一对多关系，即一个模型对应多种实现 》一致性检查 ·设计求精 llxx@ustc.edu.cn 6/112形式化开发过程 • 建立需求与系统模型之间的映射关系 – 模型获取 • 从现实世界向模型表示的转化过程 • 形式规约 – 模型验证 llxx@ustc.edu.cn 6/112 • 判断模型表示是否符合需求 • 形式证明与验证 – 模型变换 • 从模型表示向计算机系统的转化过程 – 一对多关系，即一个模型对应多种实现 » 一致性检查 • 设计求精