基于机器学习正确性属性的信息物理系统轻量级验证与确认

自主信息物理系统要真正进入社会应用、要通过美国国防部的认证使用，验证与确认（verification and validation）是一道绕不过去的关卡。这份由 Matthew L. Litton 在 Naval Postgraduate School 完成的计算机科学博士论文，讨论的正是这道关卡上最费力的环节：传统形式化 V&V 必须先写出一套形式化规范，把系统行为、性能和可靠性的要求僵硬地刻画出来，而这件事本身就极其昂贵。论文要回答的问题是，能不能不再依赖人工从头编写形式化规范，改用机器学习得到的正确性属性（machine-learned correctness properties）来完成验证与确认。在自主系统快速落地、而形式化规范供给跟不上的当下，这个提法值得认真看一眼。

研究的落点是 cyberphysical systems 与 autonomous systems，方法论上横跨 formal methods 与 machine learning 两条线，论文给出的关键词正是这四者的组合。从可公开获取的摘要看，作者走的是可行性论证的路线，而不是提出一套完整的工程流程：先指出传统路径的瓶颈在哪里，再论证机器学到的正确性属性可以承担 V&V 的职责。论文在 NPS 完成，导师为 Doron Drusinsky，公开版本按 Distribution Statement A 发布，可无限分发。需要说明的是，摘要层面的材料并未给出具体的实验平台、数据集或案例规模，方法的操作细节只能从摘要的框架描述中去把握。

论文对现状的判断可以拆成两条。第一，传统形式化 V&V 的困难不在于验证算法本身，而在于前置的形式化规范必须把系统行为、性能与可靠性写成刚性要求，这一步把大量系统挡在门外。第二，现有的形式化规范开发方法复杂且容易出错，即使对有经验的专家也难以上手——换句话说，瓶颈是人的产能，而不是工具的能力。作者据此提出的主张是：用机器学习得到的正确性属性来做验证与确认是可行的。这里的“lightweight”按字面理解，指向的应是对完整形式化规范依赖的降低，而不是验证严格性的放弃（这一点属于解读，摘要本身未展开）。

第三个值得注意的构件是 advance-notice oracles。摘要指出，这类 oracle 可以用来预测内部或外部故障，从而在开发、测试和运行三个阶段都给出系统行为的持续保证。这一点比“可行性”更进一步：它把 V&V 从发布前的一次性关卡，延伸成贯穿生命周期的连续判断。如果这一机制成立，验证活动的产出就不再只是“通过/不通过”的结论，而是对故障的提前预警（这是解读）。

把这些放在一起看，这份研究的意义在于改变了规范问题的提问方式。当正确性属性可以由数据学习得到，规范就从必须由人预先写死的前置条件，变成可以训练、可以迭代的对象，专家的精力也从编码规范转向定义学习目标与判断属性是否可信——这是解读，但也是摘要三条要点自然导出的方向。对实践者而言，advance-notice oracles 的概念尤其有操作性：它提示验证能力可以部署到运行期，而不只是留在测试台上。

这份论文适合做形式化方法、自主系统测试与机器学习交叉方向的读者，也适合在工程实践中被规范编写成本卡住的人。读完可以拿走的是一套问题框架：传统 V&V 的瓶颈定位、机器学习正确性属性作为替代路径的可行性主张，以及 advance-notice oracles 这一贯穿开发与运行的概念工具。边界同样需要点明：可获取的摘要只停留在可行性层面，没有给出量化对比，因此不能据此认为该方法已优于传统形式化路径；单篇博士论文的验证范围有限，具体结论仍需回到全文与后续工作去核对。

LIGHTWEIGHT VERIFICATION AND VALIDATION OF CYBERPHYSICAL SYSTEMS USING MACHINE- LEARNED CORRECTNESS PROPERTIES Title LIGHTWEIGHT VERIFICATION AND VALIDATION OF CYBERPHYSICAL SYSTEMS USING MACHINE-LEARNED CORRECTNESS PROPERTIES Item Type Thesis Authors Litton, Matthew L. URI https://hdl.handle.net/10945/73604 Publisher Monterey, CA; Naval Postgraduate School Date Issued 2024-09 Rights This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States. Download date 2026-11-04 22:58:41 Link to Item https://hdl.handle.net/10945/73604 Downloaded from NPS Archive: Calhoun NAVAL POSTGRADUATE SCHOOL MONTEREY, CALIFORNIA DISSERTATION L IGHTWEIGHT VERIFICATION AND VALIDATION OF CYBERPHYSICAL SYSTEMS USING MACHINE-LEARNED CORRECTNESS PROPERTIES by Matthew L. Litton September 2024