在学习形式化方法之前，先来看这样一道题：
题目：电梯控制系统规格说明
某建筑物内有一台电梯，楼层编号为1至N（N≥2）。电梯有两种运行模式：正常运行模式和检修模式。在正常运行模式下，电梯接收用户按下的楼层请求，按照电梯调度算法逐层移动，到达请求楼层后开门，停留5秒后关门，继续响应下一个请求。当电梯处于运动状态时，外部按下的同一方向的楼层请求应当被加入请求队列。在检修模式下，电梯只响应检修人员的指令，不响应普通用户请求。
请使用形式化方法描述这个电梯控制系统的行为，并说明如何验证系统不会出现“在同一时间既开门又关门”的矛盾状态。
这个题目看起来是一个常见的电梯控制系统描述，但如果用自然语言来写规格说明，很容易出现矛盾、二义性和不完整性的问题。这正是为什么需要形式化方法的原因。
2. 什么是形式化方法？
在进入解题思路之前，先来了解一下形式化方法的概念。
形式化方法是基于逻辑和数学的原则化方法，用于系统的规范、建模、设计、验证等环节，旨在构建正确且可构造的系统并提供可证明保证。在软件工程领域，它以数学理论为基础，通过形式化规格描述与验证来开发计算机系统，核心目标是为软件设计构建精确的数学模型，消除自然语言描述的歧义性，覆盖从需求分析到测试的全生命周期。
形式化方法的描述方式主要分为两类：
模型描述（Model Description）：通过构造状态机、代数结构或进程网络来刻画系统的行为结构，重点在于“系统由哪些状态、如何迁移”。常见的有有限状态机（FSM）、Petri网、进程代数等。
性质描述（Property Description）：通过逻辑公式或断言来声明系统必须满足的约束，比如“不会死锁”“所有请求最终被响应”。常用手段有线性时序逻辑（LTL）、计算树逻辑（CTL）、霍尔逻辑等。
也就是说，模型描述是“画系统长什么样”，性质描述是“规定系统必须满足什么规矩”。
3. 解题思路
回到上面的电梯系统例题，我们的解题思路分为三步：
第一步：确定建模方法
电梯控制系统天然适合用有限状态机（FSM）来建模。有限状态机由状态、事件和转移构成，适合描述控制流——而电梯的“开门”“关门”“运动”“空闲”等状态正好构成一个典型的状态转移系统。
第二步：识别系统的核心状态
观察电梯在各种情况下的表现，可以抽象出以下核心状态：
空闲状态（Idle）：电梯停留在某一楼层，无待响应请求
运动状态（Moving）：电梯正在上行或下行过程中
开门状态（DoorOpen）：到达目标楼层后开门
关门状态（DoorClosing）：门正在关闭过程中
检修状态（MaintenanceMode）：电梯不响应用户请求
第三步：用数学方式描述状态迁移规则和安全性约束
对于每个状态，定义它在收到特定事件（如上楼请求、到达楼层、超时等）时如何转移到另一个状态。同时，用逻辑公式描述系统必须满足的安全性约束——例如不会同时处于开门和关门状态，不会在运动状态中开门等。这正是形式化方法的核心：用数学语言精确描述系统的行为，再用逻辑推理去验证它。
4. 代码实现与逐行解释
下面给出一个使用有限状态机来模拟电梯控制系统的Python代码示例。这份代码实现了电梯的核心逻辑，并用断言来进行基本的正确性验证。
python
from enum import Enum from typing import List, Optional # ---------- 1. 定义状态枚举 ---------- class ElevatorState(Enum): """电梯可能的状态""" IDLE = "空闲" # 等待请求 MOVING_UP = "上行" # 向上移动 MOVING_DOWN = "下行" # 向下移动 DOOR_OPEN = "开门" # 已开门 DOOR_CLOSING = "关门中" # 门正在关闭 MAINTENANCE = "检修" # 检修模式 # ---------- 2. 定义事件 ---------- class Event(Enum): REQUEST = "request" # 用户按了楼层按钮 ARRIVE = "arrive" # 到达某一楼层 DOOR_TIMEOUT = "timeout" # 开门5秒超时 DOOR_CLOSE_COMPLETE = "close_complete" # 关门完成 MAINTENANCE_ON = "maint_on" # 进入检修模式 MAINTENANCE_OFF = "maint_off" # 退出检修模式 # ---------- 3. 电梯类（核心逻辑） ---------- class Elevator: def __init__(self, total_floors: int): """初始化电梯系统。 Args: total_floors: 总楼层数 """ self.total_floors = total_floors self.current_floor = 1 # 初始在1楼 self.state = ElevatorState.IDLE # 初始状态为空闲 self.pending_requests: List[int] = [] # 待处理的楼层请求队列 self.maintenance_mode = False # 是否为检修模式 # 安全性约束：禁止同时开门和运动 self._assert_safety() # ---------- 状态转移方法 ---------- def _assert_safety(self): """验证安全性约束，确保电梯不会处于非法状态组合。""" # 约束1：电梯不能在运动状态时处于开门状态（不可能） if self.state in [ElevatorState.MOVING_UP, ElevatorState.MOVING_DOWN]: assert self.state != ElevatorState.DOOR_OPEN, \ "【安全性违规】电梯不能在运动时处于开门状态！" # 约束2：电梯不能在开门状态时处于运动状态（冗余，但包含在此） if self.state == ElevatorState.DOOR_OPEN: assert self.state not in [ElevatorState.MOVING_UP, ElevatorState.MOVING_DOWN], \ "【安全性违规】开门状态下电梯不能运动！" # 约束3：楼层范围合法性检查 assert 1 <= self.current_floor <= self.total_floors, \ f"楼层超出范围: {self.current_floor}" def add_request(self, target_floor: int): """添加一个楼层请求（事件触发）。 Args: target_floor: 目标楼层 """ # 请求楼层合法性检查 if not (1 <= target_floor <= self.total_floors): print(f"无效楼层: {target_floor}，仅支持1-{self.total_floors}楼") return # 检修模式下不响应用户请求 if self.maintenance_mode: print("⚠ 检修模式中，不响应用户请求") return # 避免重复添加同一层（简单去重） if target_floor not in self.pending_requests: self.pending_requests.append(target_floor) print(f"📋 添加请求: {target_floor}楼，当前请求队列: {self.pending_requests}") # 根据当前状态决定是否立即启动电梯 if self.state == ElevatorState.IDLE: self._start_moving() # 每次操作后验证安全性 self._assert_safety() def _start_moving(self): """根据请求队列确定运动方向并启动电梯。""" if not self.pending_requests: return # 找到第一个请求的楼层 next_floor = self.pending_requests[0] if next_floor > self.current_floor: self.state = ElevatorState.MOVING_UP print(f"🚀 从{self.current_floor}楼开始上行，目标{next_floor}楼") elif next_floor < self.current_floor: self.state = ElevatorState.MOVING_DOWN print(f"🔻 从{self.current_floor}楼开始下行，目标{next_floor}楼") else: # 当前楼层就是请求楼层，直接开门 self._open_door() def step_move(self): """模拟电梯移动一步（到达一个楼层时调用）。""" # 只能在运动状态下移动 if self.state not in [ElevatorState.MOVING_UP, ElevatorState.MOVING_DOWN]: print(f"当前状态为{self.state.value}，无法移动") return # 根据方向调整楼层 old_floor = self.current_floor if self.state == ElevatorState.MOVING_UP: if self.current_floor < self.total_floors: self.current_floor += 1 else: # MOVING_DOWN if self.current_floor > 1: self.current_floor -= 1 print(f"📍 电梯从{old_floor}楼移动到{self.current_floor}楼") # 检查是否到达目标楼层（请求队列中第一个请求的楼层） if self.pending_requests and self.current_floor == self.pending_requests[0]: print(f"✅ 到达请求楼层{self.current_floor}楼") self._open_door() # 移动后验证安全性 self._assert_safety() def _open_door(self): """开门操作。""" # 安全性：不能在运动中开门 if self.state in [ElevatorState.MOVING_UP, ElevatorState.MOVING_DOWN]: print("❌ 电梯运动中，不能开门！") return self.state = ElevatorState.DOOR_OPEN print(f"🚪 电梯在{self.current_floor}楼开门") # 开门后自动触发关门超时（模拟定时器） self._start_close_timer() self._assert_safety() def _start_close_timer(self): """模拟开门5秒后的关门超时事件。""" # 在真实系统中，这里会启动一个定时器 # 我们直接用方法调用模拟超时事件 print(f"⏰ 开门，5秒后将自动关门...") # 模拟：直接触发关门（在实际代码中应由事件触发） self.close_door() def close_door(self): """关门操作。""" # 只能在开门状态下关门 if self.state != ElevatorState.DOOR_OPEN: print("当前门未处于开门状态，无法关门") return self.state = ElevatorState.DOOR_CLOSING print(f"🚪 电梯门正在关闭...") # 模拟关门完成事件 self._door_close_complete() def _door_close_complete(self): """关门完成后的处理。""" self.state = ElevatorState.IDLE print(f"✅ 关门完成，电梯在{self.current_floor}楼空闲") # 从请求队列中移除已到达的楼层 if self.pending_requests and self.pending_requests[0] == self.current_floor: completed = self.pending_requests.pop(0) print(f"✔ 已完成请求: {completed}楼") # 如果还有未完成的请求，继续移动 if self.pending_requests: self._start_moving() self._assert_safety() def toggle_maintenance(self): """切换检修模式。""" if self.maintenance_mode: # 退出检修模式 self.maintenance_mode = False self.state = ElevatorState.IDLE print("🔧 已退出检修模式，恢复运行") # 如果有待处理请求，立即响应 if self.pending_requests: self._start_moving() else: # 进入检修模式 self.maintenance_mode = True # 强制将门关闭后进入检修状态 if self.state == ElevatorState.DOOR_OPEN: print("🔧 进入检修模式，强制关门") self.state = ElevatorState.DOOR_CLOSING self.state = ElevatorState.MAINTENANCE print("🔧 已进入检修模式，不响应用户请求") self._assert_safety() def get_status(self) -> str: """获取电梯当前状态。""" mode = "检修模式" if self.maintenance_mode else "正常模式" return f"状态: {self.state.value} | 楼层: {self.current_floor} | 模式: {mode} | 队列: {self.pending_requests}" # ---------- 4. 演示代码 ---------- if __name__ == "__main__": print("=" * 50) print("电梯控制系统 - 形式化方法演示") print("=" * 50) elevator = Elevator(total_floors=10) # 显示初始状态 print(f"\n初始状态: {elevator.get_status()}") # 添加请求 elevator.add_request(5) elevator.add_request(3) # 模拟电梯运行 for _ in range(6): elevator.step_move() # 测试检修模式 elevator.toggle_maintenance() elevator.add_request(7) elevator.toggle_maintenance() print(f"\n最终状态: {elevator.get_status()}") print("\n✅ 整个运行过程中未出现安全性违规（开门状态与运动状态未同时出现）")代码逐行解释
第1-2行：导入Python标准库中的Enum（枚举）和类型提示模块。Enum用于定义有限的状态集合。
第4-13行：定义ElevatorState枚举类。枚举中的每个值代表电梯可能处在的一个状态。使用枚举而不是普通字符串有两个好处：一是避免拼写错误，二是在类型检查阶段就能发现不存在的状态。
第15-23行：定义Event枚举类。事件是触发状态转移的外部刺激。在电梯系统中，用户按下按钮（REQUEST）、到达目标楼层（ARRIVE）、超时（DOOR_TIMEOUT）等都是典型事件。
第27-45行：定义Elevator类的初始化和基础属性。_assert_safety()是一个关键的安全性验证函数——它使用断言来检查电梯是否处于非法状态组合，比如“运动状态中门居然是开的”。这就是形式化方法中的安全性性质验证：用代码级别的断言来保证坏的事情不会发生。
第47-66行：add_request()方法——处理用户按楼层按钮的事件。在检修模式下拒绝响应用户请求（检修状态约束），并将请求加入待处理队列。如果电梯处于空闲状态（IDLE），立即调用_start_moving()启动运行。
第68-84行：_start_moving()方法——根据当前楼层和第一个请求楼层的相对位置，决定上行还是下行，完成从“空闲”到“运动”的状态转移。
第86-108行：step_move()方法——模拟电梯移动一步的过程。到达目标楼层时调用_open_door()。每移动一步后再次调用_assert_safety()，确保任何非法状态都会立即被检测出来。
第110-124行：_open_door()、_start_close_timer()和close_door()方法——实现开门→定时→关门的完整流程。注意_open_door()方法开头就检查了“不能在运动中开门”这个安全性约束，不符合时直接拒绝执行。
第126-142行：_door_close_complete()方法——关门完成后，从请求队列中移除已完成的楼层，然后检查是否还有未完成的请求。如果有，继续移动；如果没有，进入空闲状态。
第144-164行：toggle_maintenance()方法——切换检修模式，进入检修状态后忽略所有用户请求。退出检修模式时恢复到正常状态。
第166-168行：get_status()方法——返回电梯当前状态的字符串表示，方便查看。
第171-200行：演示代码——创建一个10层的电梯系统，添加楼层请求，模拟运行过程，并测试检修模式的切换。最后打印最终状态并确认整个运行过程中没有出现安全性违规。
5. 总结
通过上面的电梯系统例题和代码实现，可以梳理出形式化方法的几个关键要点：
形式化方法的核心是用数学语言精确描述系统，替代自然语言的二义性和不完整性。无论是有限状态机、Petri网，还是时序逻辑、霍尔逻辑，本质上都是在用数学的精确性来“锁定”系统的行为。
模型描述负责“画系统长什么样”。对于控制流清晰、状态有限的系统（如电梯、交通灯、ATM机），有限状态机是最直观有效的建模工具。确定核心状态、定义事件、描述状态转移规则是建模的三要素。
性质描述负责“给系统立规矩”。安全性性质（Safety）保证“坏的事情永远不会发生”，比如电梯不会同时开门和运动；活性性质（Liveness）保证“好的事情终究会发生”，比如每个楼层请求最终都会被响应。在代码实现中，断言（assert）就是对安全性性质进行运行时验证的简单方式。
代码中的安全性验证是形式化方法的工程体现。在关键的状态转移点后调用验证函数，确保没有任何逻辑错误导致系统进入非法状态。在实际工业级形式化验证中，这通常由专门的验证工具（如Dafny、TLA+、SPIN）在编译前就完成数学证明，效率远高于运行时检查。
推荐延伸阅读：如果希望深入理解如何通过模型化思维来分析和设计复杂的软件系统，推荐阅读《大象——thinking in UML》一书。这本书虽然聚焦于统一建模语言（UML），但它强调的核心思想是——用精确、系统化的模型来思考问题，这一理念与形式化方法一脉相承，可以帮助读者建立起形式化思维的坚实基础。
6. 练习网站推荐
如果想继续练习和巩固形式化方法的相关知识，可以访问以下资源：
形式化方法课程资料（中科院软件所）：https://lcs.ios.ac.cn/~zwh/fm/index.htm包含课件、模型检测工具和部分习题解答，适合系统学习
