歧义 → 错误的系统
非形式化需求在不同工程师眼中可能有不同解读。“快速”“不久之后”“稳定”——每位读者都会自行填补其中的空白；即使正确实现了被误读的需求，得到的仍是错误的系统。
自然语言需求
使能信号发出后，制动指令应在一个较短的时间内稳定。
形式化（Universal Pattern）
触发条件enable == true
动作|brake − target| ≤ 0.5
时间范围t ≤ 20 ms
已针对所有输入和标定值完成证明
模型检验 · 不存在可达的违规状态
挑战
自然语言难免留下歧义。
从书面需求到安全系统之间存在两个缺口。无论运行多少次测试，这两个缺口都依然存在。
测试 → 未解答的问题
测试只能检查您想到并尝试的行为。它无法覆盖所有输入、状态和标定值，因此，即使测试套件全部通过，真正的问题——“我的安全需求是否可能被违反？”——仍未得到回答。
测试就是抽样。 形式化验证就是证明。
形式化方法弥合两个缺口：先使需求精确，再证明代码满足该需求。
形式化规约
一种直观的语言。
BTC Universal Pattern 是一种图形化、直观的需求工程方法——编辑器与文档是同一份成果。您描述必须成立的条件；工具将其转换为机器可读形式，并在整个过程中保留与源需求的可追溯性。
将需求转化为机器可读形式的三个步骤
1识别
标记表达式
标记需求中有意义的短语，并将其转换为可复用的宏。
在 [使能] 后，
[制动稳定]
2结构
组织结构并设定时间关系
以图形方式将宏组织为触发条件、动作和时间关系——该模式可消除歧义。
触发条件：使能
动作：制动稳定
20 ms 内
3映射
连接至接口
将每个宏与真实系统信号绑定。此时，需求即可被机器读取和执行。
enable → ctrl.en
brake → act.trq
✓ 机器可读
每一步都会保留与源需求之间的双向可追溯性。
可信人工智能
AI 辅助形式化——补齐缺失环节。
手工编写形式化规约曾是一项挑战。从根本上说，将需求形式化是一项语言任务——这恰恰是现代 AI 所擅长的。
BTC AI Assistant 根据书面需求起草包含触发条件、动作和时间关系的 Universal Pattern，供您进一步完善、批准或据此生成测试用例。
形式化验证
验证流程中的 3 个用例。
机器可读需求 = 自动验证。
01
形式化测试
一次性将每个现有测试用例与每项形式化需求交叉核对——无需额外工作，即可发现测试原本未被设计用于检测的副作用。
02
自动测试生成
模型检验可准确生成测试套件中缺失的测试用例，以确定性方式将需求覆盖率提升至 100%，而非依靠反复试验。
03
形式化验证
模型检验会给出数学证明，表明某项需求永远不会被违反——任何输入与标定值的组合都无法到达不安全状态——或者返回一个具体反例。
核心优势
形式化方法能为您带来什么。
更完善的需求
形式化促使需求变得精确——在代码和测试产生之前即可发现模糊需求。
有意义的覆盖率
自动测量并补齐需求覆盖率，而非依靠估算。
副作用检测
将每项测试与每项需求逐一核对——无需额外工作，回归问题便会显现。
100% 覆盖率
自动生成的测试向量可补齐缺口，实现完整的需求覆盖率。
100% 证明
对所有输入和标定值均成立的保证。