形式化方法

• 定义：基于严格数学与逻辑，对系统做无歧义、可验证的精确描述与证明的软件工程方法。
• 定位：UML 是半形式化建模语言；形式化方法是完全数学化的严谨规范手段。
• 核心：形式规约（精确定义系统行为）+形式验证（数学证明正确性）。
• 作用：消除歧义、提前发现逻辑漏洞，保障高可靠系统安全稳定。
• 关系：UML 负责可视化建模，形式化方法负责逻辑严谨校验，二者互补。

形式化方法发展历程

1. 萌芽期（20 世纪 50-60 年代）

   程序逻辑、数理逻辑理论兴起，学者开始用数学方法描述程序，奠定理论基础。

2. 起步期（20 世纪 70 年代）

   正式提出形式化规约概念，出现各类形式化描述语言，初步应用于小程序与理论验证。

3. 发展期（20 世纪 80-90 年代）

   技术走向实用化，工具逐步成熟，广泛用于航空、军工、金融等高可靠安全领域；同时与 UML 等建模技术结合。

4. 普及融合期（21 世纪至今）

   轻量化形式化方法出现，融入软件工程全流程，和建模、敏捷开发、自动化测试结合，从专用领域走向通用软件开发。

形式化方法应用领域

1. 安全关键领域：航空航天、轨道交通、核电、工业控制，规避致命故障。
2. 金融领域：支付系统、交易平台、区块链，保障数据与交易安全。
3. 军工 / 国防：军用软硬件、通信系统，提升系统可靠性与保密性。
4. 嵌入式系统：智能设备、车载系统、物联网终端。
5. 芯片与硬件设计：集成电路、处理器，验证电路逻辑正确性。
6. 通用软件：操作系统核心、编译器、数据库等基础软件。

‍