形式化方法(Formal Method) ·定义： 一用离散数学的方法建立系统的精确数学模型，并对模型进行分析。 ·集合论、图论、代数结构、组合数学、数理逻辑。。。 一运用形式化语言，进行形式化的规格描述、模型推理和验证。 ● 目的：保证系统设计的正确性 -保证规格说明的无二义性 ·使得证明和验证系统实现满足用户和系统需求成为可能。 -检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 。 效益 一系统代码规模 ·1979年，哥伦比亚航天飞机4000万行(2001年，XP3500万行) -非形式化技术：软件故障率2~一20个/千行代码 -形式化技术：软件故障率0.75个/千行代码(1992年，英国民航局信 息显示系统) llxx@ustc.edu.cn 5/112形式化方法（Formal Method） • 定义： – 用离散数学的方法建立系统的精确数学模型，并对模型进行分析。 • 集合论、图论、代数结构、组合数学、数理逻辑。。。 – 运用形式化语言，进行形式化的规格描述、模型推理和验证。 • 目的：保证系统设计的正确性 – 保证规格说明的无二义性 • 使得证明和验证系统实现满足用户和系统需求成为可能。 llxx@ustc.edu.cn 5/112 • 使得证明和验证系统实现满足用户和系统需求成为可能。 – 检查模型的一致性，推导模型的逻辑结果，模拟/执行模型等 • 效益 – 系统代码规模 • 1979年，哥伦比亚航天飞机4000万行（2001年， XP 3500万行） – 非形式化技术：软件故障率2～20个/千行代码 – 形式化技术：软件故障率0.75个/千行代码（1992年，英国民航局信 息显示系统）