model-checking

2热度

1回答

如何获取UPPAAL中的时钟当前值并将其存储在整型变量中？

任何人都可以告诉我如何获取时钟变量的当前值并存储在整数变量中。我试过k = t（其中k是整数，t是时钟），但它会抛出“不兼容的类型错误”。我也尝试过k =（int）t，但它引发了“意外的T_INT”语法错误。 是否有任何类型转换可用于UPPAAL中的时钟以获取时钟的当前值并将其存储在变量中？

model-checking 2011-11-11

---

1热度

1回答

从Spin Modelchecker了解错误路径

我试图使用自旋模型检查器来模拟两个对象（A和B）之间的游戏。物体在板上移动，每个位置由其（x，y）坐标定义。这两个物体应该不会相撞。我有三个进程：init，A Model，B Model。我的模型检验的LTL性质：（活跃度属性来检查，如果两个物体永远占据相同的位置） ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) } 错误线索，我得到的是： 初始

model-checking spin 2012-04-13

---

0热度

2回答

如何将序列分配给TLA +配置文件的CONSTANTS部分中的常量？

我试过 CONSTANTS seq = <<5,6,7>> 但TLC给了我一个语法错误： Error: TLC found an error in the configuration file at line 1. It was expecting = or <- and didn't find it. 我也试着包括配置文件中Sequences模块，都无济于事。 那么......我需要做些什么

configuration constants model-checking tla+ tlc 2010-05-21

---

4热度

1回答

自旋 - 形式化验证

有没有人有这个工具SPIN，甚至更多的model checking（并发程序）的任何信息

model-checking spin 2011-05-17

---

5热度

3回答

模型检查大型分布式C++项目（如KDE）的工具？

是否有一种工具可以处理模型检查大型的现实世界中大多数为C++的分布式系统，比如KDE？ （KDE是一个使用IPC的分布式系统，尽管通常所有进程都在同一台机器上。顺便提一句，这是“分布式系统”的有效用法 - 检查维基百科。 ） 该工具需要能够处理内部进程事件和进程间消息。 （让我们假设，如果该工具支持C++，但不支持KDE使用诸如MOC其他的东西，我们能砍东西一起要解决这一点。） 我会很乐意接受少将

c++ static-analysis formal-methods formal-verification model-checking 2010-11-10

---