大家好，欢迎来到IT知识分享网。
参考视频：
- 形式化验证的原理与新应用
- 【DatenLord达坦科技】形式化验证入门(我强推！！！！！)
int cnt = 0; void add(num){
if(num>=10)报错; else cnt+=num; } 
模糊测试TODO
结合LLM
LTL
LTS的乘积
LTP
安全性&不变性(safety & invariant)
所以就是在有限字上找一个坏前缀(有限步骤上会不会有坏状态，如果当前已经坏了，那么后面肯定就不能走了)
活性(liveness)
有几种，比如最终发生一次，会发生多次最终发生一次，每次等待了就一定能发生
LTL
- 安全性：线程P1和P2不会同时进入临界区： G ( ! ( c r i t 1 & c r i t 2 ) ) G(!(crit_1 \& crit_2)) G(!(crit1&crit2))
- 活性：两个线程最终都能进入临界区，不会饥饿： ( G ( F ( c r i t 1 ) ) & G ( F ( c r i t 2 ) ) ) (G(F(crit_1))\&G(F(crit_2))) (G(F(crit1))&G(F(crit2)))
- 强活性：只要等待了就最终能进去：
例子：下图表示
- 外面包着G，表示每一跳都保持这个属性
- 先红灯，然后红灯亮一会，最终变黄灯
- 黄灯也亮一会，最终变绿灯
CTL
将需求规范形式化
工程实践
TLA+
demo
进一步改进
把or再改下
TLA真实代码
免责声明：本站所有文章内容,图片，视频等均是来源于用户投稿和互联网及文摘转载整编而成，不代表本站观点，不承担相关法律责任。其著作权各归其原作者或其出版社所有。如发现本站有涉嫌抄袭侵权/违法违规的内容,侵犯到您的权益，请在线联系站长,一经查实,本站将立刻删除。 本文来自网络,若有侵权，请联系删除，如若转载，请注明出处：https://haidsoft.com/114633.html
