问题标签 [formal-verification]

我正在检查软件的模型一致性。为此，我需要为 UML 2.0 序列图编写线性时序逻辑。如果任何机构有任何其他相同的工具，请尽快回复。我会很感激你的。我发现迷人的工具有相同的插件。有没有人有魅力工具的源代码（检查建筑模型一致性）。它在他们的网站上不可用。

提前致谢。

如果不对 ring0 中运行的程序进行正式验证，如何确保安全性？可以在没有不同用户空间内核空间的情况下使用 VM 吗？

我在大学里学习过形式系统，但令我失望的是，它们似乎并没有真正用于现实世界。

我喜欢能够知道某些代码（对象、函数等）工作的想法，而不是通过测试，而是通过证明。

我相信我们都熟悉物理工程和软件工程之间不存在的相似之处（钢的行为可以预测，软件可以做任何事情——谁知道呢！），我很想知道是否有任何语言可以可以在实际中使用（要求 Web 框架要求太多了吗？）

我听说过有关 scala 等函数式语言的可测试性的有趣事情。

作为软件工程师，我们有哪些选择？

从以下想法继续：是否有任何可证明的现实世界语言？

我不了解你，但我厌倦了编写我无法保证的代码。

在问了上述问题并得到了惊人的回应（谢谢大家！）之后，我决定缩小对Haskell的可证明的、实用的方法的搜索范围。我选择 Haskell 是因为它实际上很有用（为它编写了许多 Web 框架，这似乎是一个很好的基准），而且我认为它在功能上足够严格，可以证明，或者至少允许测试不变量。

这就是我想要的（但一直找不到）

我想要一个可以查看 Haskell 函数的框架，添加，用伪代码编写：

- 并检查某些不变量是否适用于每个执行状态。我更喜欢一些正式的证明，但是我会满足于模型检查器之类的东西。
在此示例中，不变的是给定值a和b，返回值始终是总和a+b。

这是一个简单的例子，但我不认为这样的框架不可能存在。可以测试的函数的复杂性肯定会有一个上限（一个函数的 10 个字符串输入肯定会花费很长时间！）但这会鼓励对函数进行更仔细的设计，并且与使用其他形式的函数没有什么不同方法。想象一下使用 Z 或 B，当您定义变量/集合时，您要确保为变量提供尽可能小的范围。如果您的 INT 永远不会超过 100，请确保将其初始化！像这样的技术和适当的问题分解应该——我认为——允许对像 Haskell 这样的纯函数式语言进行令人满意的检查。

我对形式化方法或 Haskell 的经验还不是很丰富。让我知道我的想法是否合理，或者您认为 haskell 不适合？如果您建议使用不同的语言，请确保它通过了“has-a-web-framework”测试，并阅读原始问题:-)

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

（KDE 在使用 IPC 的意义上是一个分布式系统，尽管通常所有进程都在同一台机器上。是的，顺便说一句，这是“分布式系统”的有效用法 - 检查 Wikipedia。）

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

（假设如果该工具支持 C++，但不支持 KDE 使用的其他东西，例如 moc，我们可以一起破解一些东西来解决这个问题。）

我很乐意接受不太通用的（例如，专门用于查找特定类别错误的静态分析器）或更通用的静态分析替代方案，以代替实际的模型检查器。但我只对能够实际处理 KDE 规模和复杂性项目的工具感兴趣。

是否有一种正式的独立于语言的语言来描述 API？我想定义一个跨多个架构使用的实用程序库，并希望以某种方式以编程方式测试所有 API 函数是否已实现，并且理想情况下，跨平台运行函数的一些单元测试。

例如，我想用 C# 写一个 .Net 程序集，用 C++ 写一个 Windows DLL，用 Objective-C 写一个 MacOS 库，用 C++ 写一个 Linux 共享库。

这是一个简单的图形操作方法，我用代码契约装饰了它。

确保声明无法证明，但我不明白为什么！我相信它声称在调用 Remove() 之后，边缘不再在边缘列表中，或者结果为假。如果结果为真，它不会声明图的状态。静态检查器不喜欢它，我还没有让 Pex 告诉我如何（尽管我可能只是不知道如何使用它）。

我相信这个例子中的锁是无关紧要的，但我会留下它以防万一。此外，OnRemoveEdge 的委托没有任何保证，但我现在隐含地假设它不会重新进入 Graph 代码。此外，假设是在它之后。

更新：我更改了代码以将事件处理程序 OnRemoveEdge()（但不是委托 OnBeforeRemoveEdge）移出锁定。但是，这对合约与线程相关的假设有什么作用呢？代码契约是否假设为单线程模型？嗯。

我有兴趣证明一些机器人控制器没有达到任何故障状态，我将通过一组谓词来定义它。我知道有开源软件工具可以实现这一目标。例如，我听说过BLAST（Berkeley Lazy Abstraction Software Verification Tool），但您是否知道任何其他可能更易于使用和/或更针对我的特定应用程序的工具？

您是否曾经在您的一个项目中使用过 BLAST 或其他此类工具，您是否认为收益超过部署此类工具所需的努力？

我是 Frama-C 的新手用户，对指针断言有一些疑问。

考虑以下涉及的 C 片段：

• 两个相关的数据结构Data和Handle，st Handle有一个指向Data的指针；
• 数据中的“状态”字段，指示某些假设操作是否已完成
• 三个函数：init()、start_operation() 和 wait()；
• 使用上述方法的 main() 函数，并包含 6 个断言 (A1-A6)

现在，为什么 A5 和 A6 不能用 WP 验证程序断言（“frama-c -wp file.c”）由于 start_operation() 上的最后一个“ensures”子句，它们不应该成立吗？

我究竟做错了什么？

最好的，

爱德华多

SMT 求解器是为处理类似于 SAT 的可满足性而开发的。众所周知，SAT 也是可满足性的，并且提出了 SAT 的变体。其中之一是 max-SAT。所以我想问一下是否存在 max-SMT 求解器，如果存在，它是如何工作的？