学习笔记：形式化方法与《大象——Thinking in UML》

一、形式化方法

形式化方法是基于数学逻辑的软件工程技术，核心是用严谨的数学模型描述、分析和验证软件系统，消除自然语言的歧义，证明系统满足关键性质（如安全性、可靠性）。

核心特点：以形式化语言构建无歧义的系统规格，通过模型检测、定理证明等技术验证正确性。

适用场景：航空航天、金融安全等高可信领域，用于验证关键模块的正确性，而非全流程通用。

二、《大象——Thinking in UML》

这本书并非单纯的UML语法手册，而是传递“用UML建模思维理解业务”的核心理念：

建模的本质是沟通需求、梳理业务逻辑，而非机械绘制图形；

从用例分析到类图设计，完整呈现面向对象分析与设计的流程；

帮助建立“业务驱动模型”的思维，避免为了画图而画图。

小结

形式化方法代表了软件工程的严谨性，而UML建模则是连接业务与技术的桥梁。二者共同指向一个目标：让软件设计更清晰、更可靠。