一、什么是形式化方法
形式化方法是软件工程、计算机领域里，基于严格数学逻辑的系统开发与验证技术。
简单来说：
1. 用数学语言、形式逻辑、自动机等理论，精准描述软件/硬件系统的需求、规则和运行行为，避免自然语言带来的歧义；
2. 可以通过数学推导、逻辑证明，提前验证系统设计的正确性、一致性和安全性；
3. 多用于航空、高铁、航天这类高安全、高可靠要求的关键系统开发，大幅降低软件出错的风险。
二、《大象——Thinking in UML》阅读心得
这本书最打破认知的一点：UML不是画图工具，而是面向对象的思考方式。
它不是机械教我们画UML各种框图，而是带着完整的项目案例，从头到尾演示：
- 如何从杂乱的业务需求里梳理清楚边界、角色与核心目标
- 如何用面向对象思维抽象业务、搭建系统模型
- 如何用建模打通从需求分析、系统设计到落地开发的完整链路
读完明白：建模的本质，是理清思路、统一团队认知，图形只是思维落地的载体，好的设计永远先有清晰的思考，再产出规范的模型。
三、个人小总结
形式化方法追求严谨、精准、可验证，保障系统不出错；
UML建模则偏向抽象、梳理、可视化，解决复杂业务的理解与设计难题。
两者相辅相成：先靠面向对象建模理清业务与架构，再用形式化方法做关键环节的严谨校验，是打造高质量、高稳定性软件的优秀思路。
