Day1-6测试积点任务
问题:【模型检测问题】设计一个系统,采用递归模型,如何验证某一个给定的性质?
模型检测问题:设计一个系统,采用递归模型,如何验证某一个给定的性质
目前思路:使用基于自动机的语义模型,尝试借用spin和LTL。
困惑:由于是递归模型,因此使用自动机来表达时,递归执行后会有很多个自动机(调用自身的状态机),整个系统的状态可能是无穷个,这对spin来说不适用,但既然是递归,模型里面很多都是类似的状态和迁移,一层一层的,是否可以借用spin?或者有没有其它更好的思路?
在验证的部分,加入检查点设置 设计检查点 加检查点 加检查点 没有别的好的办法,只能根据算法,自己设计,然后根据运行加入验证检查
页:
[1]