问题标签 [formal-verification]

I used to verify a module that consists of a serial port with a set of registers by dynamic tests. One of the test is a restore reset test. The timing sequence is (i) write a random data into a register from serial port (took 40 clock cycles) (ii) put this register in reset and release it (iii) read this register from serial port (took another 40 clock cycles)

This is easily implemented in a dynamic test. Now I want to write this timing formally, but I found formal tools struggled to determine this assertion as the timing is so long, about 82 cycles, the formal tools could not explore so many space states. Is it possible to write such a test formally?

Moreover, the common reset formal test is simple, which takes 1 cycle only, the formal tool start to explore the space states from the state of reset. But now I am trying write a test that saying after the DUT did something, put the reg in reset, read it out, the value is still the reset value.

这个证明在 Dafnys 的验证器中给出了一个无限循环：

这指向某种不确定性问题还是它？有没有更好的方法来呈现这个问题以避免无限循环？

以前的版本：

这可能会去 cs 或 cstheory 堆栈交换，但我在这里看到了带有正式验证标记的大多数问题。

是否有大量关于使用指称语义进行程序验证的文献？

通过快速搜索，我发现

沃尔夫冈·波拉克。基于指称语义的程序验证。在第八届 ACM 编程语言原则研讨会的会议记录中，第 149-158 页。ACM，1981 年 1 月。

http://www.pocs.com/Papers/POPL-81.pdf

程序验证的基础，第 2 版 Jacques Loeckx，Kurt Sieber ISBN：978-0-471-91282-8

这门课程：

https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/

此外，是否有使用指称语义的某些语言的实用程序验证工具？

我一直在研究 Dafny 中引理的使用，但发现很难理解，显然下面的示例无法验证，很可能是因为 Dafny 没有看到归纳法或类似引理的东西来证明计数的某些属性? 基本上，我不知道我需要如何定义或定义什么来帮助说服 Dafny 计数是归纳性的等等。一些确保和不变量规范不是必需的，但这不是重点。顺便说一句，这在 Spec# 中更容易。

假设我们有以下 C 代码：

我想在初始化时使用静态分析计算变量 x 的边界，从而得到满足的谓词。在这个例子中，main 开头的 x 的间隔应该是 [8, 12]。

TL;DR：给定代码中某处的断言，计算这些范围的最佳方法是什么？

到目前为止我尝试了什么：

我认为解决这个问题的最佳方法是使用最弱的前提条件计算器。我尝试过使用 frama-c 的 wp 插件，但由于它是为验证目的而构建的，我不确定它在这个用例中有多有用。在以下代码上应用插件时：

我收到以下谓词发送到 alt-ergo 求解器：

如果您仔细观察，可以通过遵循变量 i 上不会导致 (i_1 = 0) 的边界来识别输入所需的间隔。我已经标记了这些界限。这不是很健壮，例如，如果断言更改为&& n <= 13，则隐含谓词的“左侧”保持不变，因为没有任何条件改变。另外我不确定这在其他情况下有多大用处，例如在调用函数时将我的断言更改为 requires 语句，我无法理解生成的谓词：

并向函数添加 requires 语句：

我得到：

我一直在阅读有关形式验证的内容，基本观点是它需要一个正式的规范和模型才能使用。然而，许多来源将静态分析归类为一种形式验证技术，一些提到抽象解释并提到它在编译器中的使用。所以我很困惑——如果没有模型的正式描述，这些怎么可能是形式验证？
编辑：我发现的一个来源是：

静态分析：抽象语义是根据预定义的抽象从程序文本中自动计算出来的（有时可以由用户自动/手动定制）

那么这是否意味着它只适用于源代码而无需正式规范？这就是静态分析器所做的。

另外，如果没有形式验证，是否可以进行静态分析？例如，SonarQube 真的执行形式化方法吗？

最近我读了很多关于形式验证的文章，我对这个话题很着迷。但是我无法弄清楚以下内容：
形式验证需要形式规范，那么当程序没有形式规范时，如何在编译器中的任何源代码上使用抽象解释？

从看起来正确的外语文本翻译（而且似乎不需要正式的规范。）

如果一个程序由它的控制流程图表示，那么每个分支都表示一个程序状态（可以不止一个 - 例如，在循环中，一个分支被遍历多次）并且抽象解释创建了近似于该状态集的静态语义。

这里有一篇关于抽象解释作为形式验证技术的文章：http ://www.di.ens.fr/~cousot/publications.www/Cousot-NFM2012.pdf

我正在使用 Windows 操作系统并在 Cygwin 中输入：wish -f ispin.tcl打开 ispin 界面。我打开一个文件test.pml，其中包含：

之后，我使用种子 = 123 的随机方式运行它。结果打印在输出中没有问题：

当我尝试验证此模型时出现问题。验证结果为：

我该如何解决这个问题？我在互联网上搜索，但找不到可以帮助我的东西。

注意：我没有更改任何验证属性：

我有一个数组line，其中包含一个长度为 的字符串l， pat是另一个数组，其中包含一个长度为 的字符串p。注意：pandl不是数组的长度

目的是查看 中包含的字符串是否pat存在于 中line。如果是这样，这个方法应该返回line单词第一个字母的索引，如果不是，它应该返回-1。

给我们“没有发现触发”错误的不变量是ensures exists j :: ( 0<= j < l) && j == pos;和invariant forall j :: 0 <= j < iline ==> j != pos;

我对循环的逻辑是，当它们在循环中时，找不到索引。并且确保它遇到索引时。

有什么可能是错的？

这是代码：

我收到以下错误： Dafny 输出的屏幕截图

这是rise4fun 上的代码。

我有一个数组“line”，其中包含一个长度为“l”的字符串，还有一个数组“nl”，其中包含一个长度为“p”的字符串。注意：“l”和“p”不一定是每个对应数组的长度。参数“at”将是在“line”内进行插入的位置。恢复：长度为“p”的数组将插入“line”，将“line”的所有字符在位置（at，i，at+p），'p'位置之间向右移动以进行插入。

我的确保逻辑是检查插入“line”中的元素是否具有相同的顺序并且是否与“nl”中包含的字符相同。

这是代码：

这是 我收到的错误。

谢谢。