温度低于5度或高于45度就算进入紧急状态,规格要求系统必须在10个时间单位内把温度拉回15到35度这个正常区间。湿度也不是随便定的:只要温度落在15到35度,湿度就必须保持在20%到80%之间。这些规则不是写在需求文档里等人肉核对,而是用一种叫Lilo的语言写成代码,直接丢进 VSCode 里做分析,像跑测试一样看它通没通过。
这份材料是 SpecForge 的用户导览,讲的是一套能力清单,不是新品发布或市场消息。但它想解决的问题值得琢磨:形式化方法这套东西,多年来一直是学术圈和少数安全关键领域的专属工具,门槛高、上手慢。SpecForge 想把它塞进日常开发流程,让写规格变得跟写代码一样顺手。
写规格用的是一门时序语言
Lilo 面向混合系统,基础类型和运算符都很常规,真正的核心是时序算子:always(始终成立)、eventually(终将成立)、past(曾经成立)、historically(一直曾经成立),还能加时间区间限定,比如 eventually[0,10] 就是“10个时间单位内成立”。系统文件用 system 声明,把 signal(随时间变化的输入)、param(不随时间变化的参数)、type、def、spec 组织在一起。温湿度控制那个例子,就是这套语法的最小可用形态:十几行代码,定义了信号、边界、紧急状态判断和恢复要求。VSCode 插件负责语法高亮、类型检查和可满足性提示,写错了当场标红,不用等跑完分析才发现。
写完规格,能拿它做什么
规格写完之后,SpecForge 提供几类分析:监测(Monitor)拿一段已经录好的系统轨迹去核对规格是否满足;示例生成(Exemplify)反过来生成一条满足规格的样本轨迹,帮你确认“规格写的到底是不是你想要的东西”;反例搜索(Falsify)需要额外接入系统模型和 falsifier 配置,专门找违反规格的行为;导出能把规格转成 JSON 等格式给别的工具用,可视化则把结果画成时间线。整套流程既能在 VSCode 里点按钮完成,也能通过 Python SDK 在 Jupyter notebook 里跑脚本批量处理。对控制系统、汽车电子、机器人这类混合系统团队来说,这意味着安全需求第一次能跟数据轨迹、代码审查放进同一条流水线,而不是锁在一份 PDF 里等审计时才翻出来。
- 结论.把需求、数据轨迹和反例拉进同一条开发链,是这份指南最实在的价值。
分析通过不是证明
三种分析的底气不一样。监测只能证明“录到的这段数据没违反规则”,没录到的场景一律不知道;示例生成本质是给规格本身做体检,检验的是你的意图,不碰真实系统,规格写错了它照样能生成一条“合规”的假轨迹;反例搜索最接近正统形式化验证,但前提是先有一个系统模型,还得额外写 falsifier 脚本接进 specforge.toml,门槛比前两者都高——而它检验的是“模型”符不符合规格,模型建错了,分析照样一路绿灯。
分析通过,替代不了正确的规格。
- 风险.规格写错或漏掉边界条件,分析照样能显示“通过”,团队容易把“跑通”误读成“系统已被证明安全”。
温湿度控制器那道十几行代码之所以好懂,正是因为够简单。真正的混合系统规格,边界条件成百上千,漏一条比多写一条更容易发生。SpecForge 把“写规格”这件事的门槛拉到了工程师能够着的高度,这是它值得认可的地方;至于规格立不立得住,还得靠人。荀子说“尽信书,不如无书”,放在这儿也合适——工具越顺手,越不能把分析结果当成不假思索的免死金牌。