标签: model-checking

正如标题所说,Coq可以用作模型检查器吗？我可以将模型检查与Coq证明混合使用吗？这通常吗？谷歌谈到"微积分",有没有人有这种或类似的经验？建议以这种方式使用Coq,还是应该寻找其他工具？

我目前正在学习模型检查(模态逻辑,LTL,CTL,SAL模型检查器等).在我的业余时间,我正在学习Idris,这是一种支持依赖类型的强类型函数式编程语言.由于我正在研究模型检查和Idris,我开始对Idris如何与形式化方法和模型检查相关联感到好奇.

在了解模型检查时,感觉大多数示例都是关于验证以命令方式编写的系统或硬件组件.所以我对强类型函数式编程语言中的模型检查的相关性感到困惑,特别是在依赖类型的语言中,例如Idris,在我看来,类型检查器在验证正确性方面已经做了出色的工作. 然而,我的直觉告诉我,模型检查可能与不给予任何终止承诺的部分功能相关.

使用强大且依赖类型的编程语言(例如Idris)时,模型检查是否相关？

• 您使用了哪些类型的应用程序进行模型检查？
• 你使用什么模型检查工具？
• 您如何总结您使用该技术的经验,特别是在评估其提供更高质量软件的有效性方面？

在我学习的过程中,我有机会使用Spin,它引起了我对实际模型检查进行了多少以及组织从中获取多少价值的好奇心.在我的工作经历中,我从事过业务应用程序,其中(自然)没有考虑将正式验证应用于逻辑.我真的很想了解SO人员的模型检查经验和关于这个主题的想法.模型检查是否会成为我们工具箱中应该使用的更广泛使用的开发实践？

我目前正在撰写我的硕士论文,并面临着在时间逻辑中指定和验证我的方法.

在我的情况下哪种时态逻辑最好用？我真的希望对我的方法以及如何继续进行一些反馈

我的模型由参与者组成,这些参与者将同时执行.对于每个参与者,可以注册规则.他们看起来像这样:

conditions -> action

例如

received(a, c) ^ received(b,c) -> allowed(c,d) 

这意味着c必须接收来自b的消息和来自c的消息才能被允许向d发送消息.

在其中一个参与者发送或接收消息之前,我的原型检查是否允许参与者执行该操作.到目前为止,我想验证该算法是否执行以下操作:

1. 如果不存在其条件成立的规则:禁止该操作

2. 如果存在条件成立且禁止操作的规则:禁止操作

3. 如果存在条件成立的规则,则允许该操作,并且不存在其条件成立且禁止操作的其他规则:允许操作

是否有一个工具可以处理模型检查大型,真实世界,主要是C++,分布式系统,如KDE？

(KDE是一个分布式系统,因为它使用IPC,虽然通常所有进程都在同一台机器上.顺便说一下,这是"分布式系统"的有效用法 - 检查维基百科.)

该工具需要能够处理进程内事件和进程间消息.

(假设如果该工具支持C++,但不支持KDE使用的其他东西,如moc,我们可以一起破解某些东西以解决这个问题.)

我很乐意接受不太通用(例如专门用于查找特定类型的错误的静态分析器)或更一般的静态分析替代方案,而不是实际的模型检查器.但我只对能够实际处理KDE大小和复杂性项目的工具感兴趣.

我正在尝试重现Dijkstra在题为"协作顺序进程"的文章中编写的ALGOL 60代码,代码是第一次尝试解决互斥问题,这里是语法:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end 

所以我试着在Promela中重现上面的代码,这是我的代码:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn; …

CBMC在以下行中检测到可能的无符号加法溢出:

l = (t + *b)&(0xffffffffL);
c += (l < t);

我同意第一行有可能出现溢出,但我正在处理CBMC无法查看的下一行的进位.如果有溢出,我设置进位1.所以,因为我知道这个,这就是我希望我的代码工作的方式,我想继续进行验证过程.那么,我怎么告诉CBMC忽略这个错误并继续前进呢？

The "Automata View" in iSpin (v. 1.1.4) shows .. exactly what? It seems it is just a graph of the control flow of one process.

How would I get the full state space of the system?

例如，在Ben-Ari：自旋模型检查器的原理中，我想要图4.1。或在Overview中，我想要图1。

最近，我开始研究形式验证技术。在文献中，模型检查器和求解器以某种方式互换使用。但是，模型检查器和求解器是如何相互连接的？

ps 如果建议一些论文或链接，我将不胜感激。

在河流穿越Alloy模型中,这个谓词:

pred crossRiver [from, from', to, to': set Object] {
  one x: from | {
    from' = from - x - Farmer - from'.eats
    to' = to + x + Farmer
  }
}

模拟河流穿越:一侧的物体与农民一起x向from侧面移动to.

为了测试我的理解,我改变了:one x: from以lone x: from - Farmer---前移动"只有一个东西"隔江相望,后者运动"最多一个非农民的事".

我认为后者更好地模拟了这个问题:农民在平等约束中被硬编码并且总是穿越河流,并且lone应该更好地传达农民可以在河对岸采取零或一件事.

但是,在此更改后运行模型时,结果是无意义的:

在这里,第二个州的实例显示了河流两侧的鸡肉和谷物,而农民根本没有穿过.

我错过了什么？(这是在合金4.2_2015-02-22上运行的)