形式化验证笔记

news2024/11/18 22:49:40

参考视频：

形式化验证的原理与新应用
【DatenLord达坦科技】形式化验证入门(我强推！！！！！)

形式化验证：在状态机表征的空间里面进行搜索，验证某个模型是否按规范执行且测试覆盖率达到100%
方法：将规范(可选)和代码变为数学公式，再将公式放入定理证明器
在这里插入图片描述
例子

第一种作用：生成测试用例

第二种作用：验证程序是否符合规范
第一步：把控制流程图转成表达式

第二步：将规范加入表达式
但是该做法会导致只能找到正确值而不是违反规范的路径，所以要将规范取非，以匹配违反规范的情况
在这里插入图片描述
进一步，因为一般程序很复杂，所以是用验证器，让计算机进行计算

上述只能进行当前场景一次的验证，于是为了考虑时间属性，引入了LTL
比如要限制一个计数器永远小于10，下面的程序确实可以限制单次不会增加超过10，但是多次之后cnt就会超过10
所以我们就要引入G、U、F、X这种时态

int cnt = 0;
void add(num){
	if(num>=10)报错;
	else cnt+=num;
}

在这里插入图片描述

模糊测试TODO

在这里插入图片描述

结合LLM

通过LLM，使用自然语言生成规范
在这里插入图片描述

LTL

LTL主要研究的是trace，每个状态其实就是第一个label的变换
在这里插入图片描述
注意 $abc^*$ 的星号表示未知的有限次数， $abc^\omega$ 的w表示未知的无限次数

LTS的乘积

label transition system
就是两个状态机的乘积
即两边的状态做笛卡尔积
转换关系、原子命题、标签函数取并集

将待检测代码和要检查的属性(注意规范就是定义要满足的属性)，两个状态机乘起来
比如把车行灯和人行灯进行乘起来

可以看到2*3=6
在这个状态机里找有没有期待的非法状态出现
然后因为出现了{g,w}，即车绿灯时，人穿过马路
在这里插入图片描述

LTP

线性时间属性
形式化方法与数理逻辑不一样的点
即形式化方法引入了时间(离散的)概念
形式化方法因为有无限时间，所以会展开成很大的路径空间
在这里插入图片描述
我们要做的就是找到一条路径，满足我们定义的属性要求(一般就是找非法路径，没有说明程序合理)

安全性&不变性(safety & invariant)

永远不会发生坏的事情
某些属性应适用于所有可访问状态

所以就是在有限字上找一个坏前缀(有限步骤上会不会有坏状态，如果当前已经坏了，那么后面肯定就不能走了)

活性(liveness)

好事最终会发生(test case不能做到，因为测试时长是有限的)
所以是形式化验证强大的地方

通过一个有环的有限状态自动机表示一个无限序列
所以就是检查环上是否最终会出现这个好事

有几种，比如最终发生一次，会发生多次最终发生一次，每次等待了就一定能发生

LTL

注意LTL定义上只有U和F，但是衍生出了
G的意思是每一跳都要满足
F的意思是最终某一跳会满足
还有O表示下一跳
F( $\phi$ ) := True U $\phi$
G( $\phi$ ) := !(F(! $\phi$ ))
在这里插入图片描述
应用：

安全性：线程P1和P2不会同时进入临界区： $G(!(crit_1 \& crit_2))$
活性：两个线程最终都能进入临界区，不会饥饿： $G(F(crit_1))\&G(F(crit_2)))$
强活性：只要等待了就最终能进去：

例子：下图表示

外面包着G，表示每一跳都保持这个属性
先红灯，然后红灯亮一会，最终变黄灯
黄灯也亮一会，最终变绿灯

CTL

computing tree logic
计算树逻辑比LTL多了全称和存在量词，是对全局来看的
LTL就是不能表达存在某条路径，他默认带的是全称量词

将需求规范形式化

在这里插入图片描述

工程实践

在这里插入图片描述

TLA+

两种代码编写方式：TLA+和PlusCal
用状态机描述代码，有穷尽的状态

demo

在这里插入图片描述
进一步改进

把or再改下

TLA真实代码

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如若转载，请注明出处：http://www.coloradmin.cn/o/1112741.html

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈，一经查实，立即删除！