一、作业背景

       本作业是软件工程课程的阶段性学习任务，目的是帮助我们建立对软件建模方法的基本认知，理解从需求到模型的抽象过程，为后续更深入的软件设计与验证打下基础。

二、什么是形式化方法？

       形式化方法是一种以数学为基础的软件开发与验证方法，它的核心目标是消除自然语言描述中的歧义，通过精确的逻辑与模型来保证软件系统的正确性与可靠性。

1. 核心概念

数学基础：依赖集合论、一阶逻辑、自动机理论等数学工具，所有描述都可被精确定义、推导与验证。
形式化规约：使用严格的形式化语言（如 Z 语言、VDM、TLA+）描述系统需求与行为，避免模糊的自然语言表达。
验证与证明：通过模型检查、定理证明等方式，验证系统是否满足安全性、一致性等关键属性。

2. 适用场景

形式化方法多用于对可靠性、安全性要求极高的领域，例如：
航空航天、轨道交通控制系统
医疗设备、金融交易系统
操作系统内核、安全协议

3. 优势与局限

三、推荐阅读书籍：《大象 ——Thinking in UML》

       在面向对象分析与设计的学习中，《大象 ——Thinking in UML》是一本非常经典的入门读物，它跳出了 “教你画 UML 图” 的误区，重点传递面向对象思维与建模方法论。

1. 书籍核心内容

面向对象思想重构：讲解如何从面向过程思维，转变为面向对象的抽象思维，学习从需求中提炼对象、划分职责。
UML 实战应用：结合贯穿全书的实例，讲解用例图、类图、时序图等核心 UML 图的实际用法，而非单纯罗列语法。
软件全流程建模：覆盖从需求分析、业务建模到系统设计、架构设计的完整流程，教你用 UML 解决实际问题。
思维引导：打破 “UML 只是画图工具” 的认知，强调模型背后的逻辑与设计思想。

2. 阅读价值

        建立系统化的面向对象分析与设计思维，学会从业务需求中抽象出合理的对象模型。
掌握 UML 图在项目中的正确用法，用模型清晰表达系统结构、交互流程与业务规则。
理解软件建模的本质：建模不是为了画图，而是为了更好地理解问题、沟通需求与验证设计。

四、学习总结

       通过本次学习，我认识到：
       形式化方法是软件工程中保证系统正确性的重要手段，其数学基础与严谨性，对高可靠系统开发至关重要。
       UML 建模不是简单的符号堆砌，而是面向对象思维的可视化表达，核心是抽象与建模能力。
       后续我会继续阅读《大象 ——Thinking in UML》，加深对面向对象分析与设计的理解，为后续课程项目打下基础。