4. 一致性检查的规则化基础
一致性检查之所以能从“人工评审”走向“自动判定”，根本原因在于把模糊的工程意图转化成了机器可读、可推理、可复用的规则化表达。在MBSE中，这一转化并不是单一技术，而是一条由浅入深的谱系：约束（Constraint）限定取值与关系，规则（Rule）规定“什么情况算违规”，模式（Pattern）固化可复用的结构模板，契约（Contract）约定接口双方的责任与保证，本体（Ontology）提供概念与关系的公共语义，形式化表达（Formal Expression）则让上述内容具备可判定、可证明的数学基础。理解这条谱系，才能为后续的检查引擎选型、规则库建设和治理流程设计打下基础。
一、六类规则化手段的定位与分工
这六者不是互相替代，而是分层协作。约束回答“值域和关系是否合法”，规则回答“模型是否违反工程约定”，模式回答“结构是否按标准模板搭建”，契约回答“接口双方是否互相满足”，本体回答“不同模型说的概念是不是同一个”，形式化表达回答“判定是否严密、可验证”。
二、约束与规则：从“值域”到“违规判定”
约束是最贴近模型元素的规则化手段。在SysML中，约束通常以约束块（Constraint Block）或OCL表达式承载。例如，一个电池组件的质量属性约束可写为：
context Battery
inv massPositive: self.mass > 0.0
inv voltageRange: self.nominalVoltage >= 20.0 and self.nominalVoltage <= 30.0
inv cellCountMatch: self.cellCount = self.seriesCount * self.parallelCount这三条不变式分别检查质量为正、标称电压在20～30V之间、电芯总数等于串并联乘积。检查引擎在遍历模型时，对每个Battery实例求值，返回true/false。若为false，则记录违规元素、违反的约束名和当前实际值。
规则则比约束更进一步，它包含“判定条件 + 严重度 + 修复建议”。例如一条追溯性规则：
规则ID: TRC-001
适用对象: Requirement
判定条件: 不存在任何 Satisfy 关系指向该需求
严重度: Major
修复建议: 为该需求建立至少一条来自设计元素的 Satisfy 链接约束和规则的区别在于：约束是模型自身的数学性质，规则是工程治理层面的检查条目。约束可以嵌入模型，规则通常放在外部规则库中，通过模型查询接口读取模型元素后判定。
三、模式与契约：结构复用与接口责任
模式解决的是“结构是否按标准模板搭建”。例如在无人机飞控模型中，一个典型的“传感器-控制器-执行器”闭环模式要求：传感器输出端口必须连接到控制器输入端口，控制器输出端口必须连接到执行器输入端口，且三者处于同一工况上下文。检查时，引擎在模型中搜索该模式的三元组实例，若存在传感器未连接控制器的情况，则判定模式违规。
契约则聚焦接口双方的责任与保证。以供电接口为例，契约可表达为：
契约: PowerInterfaceContract
参与方: 供电方 PowerSource, 负载方 PowerLoad
前置条件: PowerSource.outputVoltage ∈ [26V, 30V]
后置条件: PowerLoad.inputCurrent ≤ 5A
不变式: PowerSource.outputPower ≥ PowerLoad.requiredPower一致性检查时，引擎分别读取供电方和负载方的属性值，代入契约条件求值。若供电方输出28V、负载方要求6A，则后置条件不满足，判定契约违规。契约的价值在于把接口一致性从“人工核对”变成“条件求值”。
四、本体与形式化表达：公共语义与可判定基础
当多个团队、多个工具、多个模型协同工作时，最大的障碍往往不是语法错误，而是“同一个词指不同东西”。本体通过定义概念、属性、关系和公理，为一致性检查提供公共语义。例如，本体中定义“接口”必须至少连接两个“端口”，“信号”必须属于某个“接口”，“工况”必须关联至少一个“系统状态”。这些公理本身就是可检查的规则。
形式化表达则让规则具备数学上的可判定性。一阶逻辑适合表达“所有需求都必须被追溯”这类全称命题；时序逻辑适合表达“在制动信号发出后，制动力必须在200ms内建立”这类时间约束；集合论适合表达“所有安全关键功能必须属于ASIL-D集合”。形式化表达的落地方式通常有两种：一是将模型元素映射为逻辑原子，用SMT求解器判定可满足性；二是将模型转换为状态机，用模型检测工具遍历状态空间。
五、落地方式：从规则条目到检查引擎
在实际项目中，这六类手段需要统一落到一个可执行的规则库中。规则库的每条记录至少包含：规则ID、规则类型（约束/规则/模式/契约/本体公理/形式化公式）、适用元模型元素、判定表达式、严重度、修复建议、版本号。检查引擎读取规则库，遍历模型元素，逐条求值，输出违规清单。
以某型无人机飞控模型为例，假设规则库中有以下三条规则：
| 规则ID | 类型 | 判定表达式（示例） | 严重度 |
|---|---|---|---|
| CON-012 | 约束 | Battery.mass > 0 | Minor |
| TRC-001 | 规则 | ∀r∈Requirement: ∃s∈Satisfy: s.target = r | Major |
| CTR-005 | 契约 | PowerSource.outputVoltage ∈ [26,30] ∧ PowerLoad.inputCurrent ≤ 5 | Critical |
检查引擎执行后，若发现某电池质量属性缺失（返回unknown而非false），应记录为“无法判定”而非“通过”，这是规则化检查中容易被忽视的边界情况。对于契约类规则，若供电方电压为25V，则CTR-005判定为违规，严重度Critical，需立即修复。
最后需要强调：规则化基础的建设应与模型治理同步推进。规则库需要版本管理，规则变更需要影响分析，规则执行结果需要与模型基线关联。只有这样，一致性检查才能从一次性脚本演化为可持续的工程能力。