写给学生看的系统分析与验证笔记（一）——形式化基础

什么是形式化验证？In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain f

Campsisgrandiflora

3560人浏览 · 2020-10-24 23:28:07

Campsisgrandiflora · 2020-10-24 23:28:07 发布

什么是形式化验证？

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

一句话概括，形式化验证是用形式化的数学方法，来证明或者反证系统满足需求规范。

为什么要用形式化验证？

航空控制系统、医疗器械、电话交换网等领域的软件或者硬件对故障较为敏感，一旦出错将会造成巨大的损失，需要一种方式来保证系统设计的正确性。

形式化验证与测试的区别

测试是寻找错误，而验证是证明正确性。

形式化验证方法

因为我们课堂上学习的主要是模型检测相关的方法，所以之后的内容以及博文都会围绕模型检测这个主题

模型检测的过程

模型检测技术

离散系统：

基于Kripke结构模型检验：SMV,nuSMV,SPIN,VIS

基于时间自动机的检验模型：UPPAAL

基于概率(统计)的模型检验：UPPAAL，Prism

混成系统：

离散、连续模型

2048 AI社区

有“AI”的1024 = 2048，欢迎大家加入2048 AI社区

更多推荐

Expect脚本实战：多条件匹配与防卡死技巧

在自动化测试和系统初始化中，我们常常使用 Expect 脚本来完成一系列交互操作，比如自动输入密码、监听输出并作出响应。然而，实际项目中可能遇到多步骤输出匹配的场景：只有在先匹配到某一行输出，再匹配到另一行输出时，才需要做出响应。同时，如果 “testX failed” 出现了，但 “set params error” 没有在合理时间内出现，不要卡死，而是打印警告并继续。这个写法的问题在于：如

2048 AI社区

AI模型版本控制的标签管理：架构师的技巧

在AI模型生命周期中，版本控制是保障模型可追溯性、协作效率与生产可靠性的核心环节。而标签管理作为版本控制的"语义接口"，其设计质量直接决定了团队对模型版本的理解、检索与复用能力。本文从架构师视角出发，结合第一性原理与MLOps实践，系统阐述AI模型标签管理的理论框架、架构设计、实现机制与高级考量。通过拆解标签的"唯一标识+语义描述"本质，提出四维标签模型。