在学习形式化方法之前先来看这样一道题题目电梯控制系统规格说明某建筑物内有一台电梯楼层编号为1至NN≥2。电梯有两种运行模式正常运行模式和检修模式。在正常运行模式下电梯接收用户按下的楼层请求按照电梯调度算法逐层移动到达请求楼层后开门停留5秒后关门继续响应下一个请求。当电梯处于运动状态时外部按下的同一方向的楼层请求应当被加入请求队列。在检修模式下电梯只响应检修人员的指令不响应普通用户请求。请使用形式化方法描述这个电梯控制系统的行为并说明如何验证系统不会出现“在同一时间既开门又关门”的矛盾状态。这个题目看起来是一个常见的电梯控制系统描述但如果用自然语言来写规格说明很容易出现矛盾、二义性和不完整性的问题。这正是为什么需要形式化方法的原因。2. 什么是形式化方法在进入解题思路之前先来了解一下形式化方法的概念。形式化方法是基于逻辑和数学的原则化方法用于系统的规范、建模、设计、验证等环节旨在构建正确且可构造的系统并提供可证明保证。在软件工程领域它以数学理论为基础通过形式化规格描述与验证来开发计算机系统核心目标是为软件设计构建精确的数学模型消除自然语言描述的歧义性覆盖从需求分析到测试的全生命周期。形式化方法的描述方式主要分为两类模型描述Model Description通过构造状态机、代数结构或进程网络来刻画系统的行为结构重点在于“系统由哪些状态、如何迁移”。常见的有有限状态机FSM、Petri网、进程代数等。性质描述Property Description通过逻辑公式或断言来声明系统必须满足的约束比如“不会死锁”“所有请求最终被响应”。常用手段有线性时序逻辑LTL、计算树逻辑CTL、霍尔逻辑等。也就是说模型描述是“画系统长什么样”性质描述是“规定系统必须满足什么规矩”。3. 解题思路回到上面的电梯系统例题我们的解题思路分为三步第一步确定建模方法电梯控制系统天然适合用有限状态机FSM来建模。有限状态机由状态、事件和转移构成适合描述控制流——而电梯的“开门”“关门”“运动”“空闲”等状态正好构成一个典型的状态转移系统。第二步识别系统的核心状态观察电梯在各种情况下的表现可以抽象出以下核心状态空闲状态Idle电梯停留在某一楼层无待响应请求运动状态Moving电梯正在上行或下行过程中开门状态DoorOpen到达目标楼层后开门关门状态DoorClosing门正在关闭过程中检修状态MaintenanceMode电梯不响应用户请求第三步用数学方式描述状态迁移规则和安全性约束对于每个状态定义它在收到特定事件如上楼请求、到达楼层、超时等时如何转移到另一个状态。同时用逻辑公式描述系统必须满足的安全性约束——例如不会同时处于开门和关门状态不会在运动状态中开门等。这正是形式化方法的核心用数学语言精确描述系统的行为再用逻辑推理去验证它。4. 代码实现与逐行解释下面给出一个使用有限状态机来模拟电梯控制系统的Python代码示例。这份代码实现了电梯的核心逻辑并用断言来进行基本的正确性验证。pythonfrom 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_floors10) # 显示初始状态 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包含课件、模型检测工具和部分习题解答适合系统学习