问题标签 [formal-methods]

我在我最新版本的罗丹平台中导入了一个完全精炼的模型，我正在尝试在这个项目中使用带有 ProB 动画师的 IUMLB。但由于该项目已经有一个预配置的 AnimB 动画师，最新的罗丹软件不支持。错误状态为“未知配置 org.animb.valuation.valBase”。

如何从项目中删除或修复此 AnimB 配置？

刚刚接触了 Microsoft 代码合同，用于检查代码中的前置条件、后置条件和对象不变量（https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts ) 并想尝试一下。我想确认一个关于健全性和完整性的问题，假设检查器不输出任何错误消息的不变量，这是否意味着该不变量确实（可证明）为真，或者它仍然可能是误报。

我正在关注 codecontracts 教程（https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines），但我似乎无法让最简单的事情正常工作. 给定方法定义

当我调用o.Add(0,0)该方法时，前置条件检查不会失败。当我处于调试模式时，Contract.Requires()会跳过这些语句。我在哪里做错了？

第二个问题可以Contract.Invariant()用来检查循环不变量吗？根据对象不变量的定义，Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client.这似乎与循环不变量有点不同，因为在每次循环迭代中，循环不变量可能不一定对客户端可见，因此它可能违反属性但未被检查。这种理解正确吗？

我想在 NuSMv 中制定这个问题：

• 用户可以处于以下三种状态之一：U-need,U-using,U-sad（表示需要服务、开始使用并且他/她对该服务的质量感到满意或开始使用并且他/她分别因为他的服务质量差而感到难过）。

• 服务可以处于以下三种状态之一：S-offer、S-good、S-bad；;（分别代表未使用的服务、提供优质服务或提供劣质服务的服务）。

• 一组事件：look,use,stop,monitor,detect-p,remedy-p，代表寻找服务、开始使用服务、停止使用服务、监控质量、检测服务中的问题并补救分别的问题。

• 这是我的 SMV 代码：

  /li>

- 我想确认这段代码代表了我上面描述的问题 - 我将服务和用户的事件和状态都表示为变量，这是否正确？

我正在 Z 中编写操作模式。此操作 AssignValue 将属性映射到一个或多个值。

一个属性可以链接一个或多个值，一个值可以链接一个或多个属性，形成多对多关系，R ⊆ 属性 × 值。

我不确定如何编写此操作以指示一个属性可以映射到一个或多个值。我这里有两个版本。版本 A 似乎将一个属性映射到一个值。

版本 A：

在版本 B 中，我在 v? 的声明中添加了一个幂集？表示 v? 是一组值（多个值）。

版本 B：

哪个版本是正确的？还是有更好的方法来表示这一点？我是 z 表示法的新手，任何帮助将不胜感激。谢谢！

我有一个操作模式 C，它由两个顺序操作模式 A 和 B 组成。必须在 B 之前执行 A。我被困在如何表示模式激活的顺序上。

我可以使用模式连词，即 C == A ∧ B 吗？或者有没有办法从A“调用”模式B？

我是 Z 表示法的新手，任何帮助将不胜感激！

我正在使用K 语义框架并运行教程，这是我的 TEST1.k ：

但是在运行命令 Komile Test1.k 时出现此错误：

ff_next关于这个合金模型的排序谓词的第一个分支，我似乎有些不明白。

这里的直觉是我有很多次曝光，每一次我都想在多个图块位置执行。考虑制作全景图像，然后将它们拼接在一起，但使用不同的相机设置多次执行此操作。

注释掉注释行后，我得到的第一个实例是：

这相当于在一张曝光的情况下通过全景图，然后将其他曝光放在地板上。

这个问题似乎是 in 之后的第一个分支=>，ff_next但我不明白出了什么问题。该分支永远不会满足，它将移动到下一次曝光和全景图的开始。如果我取消注释该行Point.ex = Exposure，模型将变得无法满足，因为它需要该分支。

关于为什么该分支不能满足的任何帮助？

我是一名软件工程师/架构师，专注于人工智能和分布式系统，我来自电子和通信工程背景。

在我的软件之旅中，我一直想知道为什么这个工程分支缺乏正式的设计方法，如电子学（数学建模和实现）以及具有许多约束的最佳通信系统的设计，这些系统中的大多数都是比地球上最复杂的软件（比如运行我们使用和开发的软件的 IC）复杂得多，并且唯一具有正式方法的软件相关领域是硬件描述语言。

我最近了解到，存在用于软件设计、规范和验证的形式化方法，如 Z 符号和语言、维也纳开发方法和 b 语言。

但是这个领域的最新技术是什么，普通工程师如何使用它（例如在我的团队中）？

MathWorks 有一个名为 Polyspace Code Prover 的形式验证工具。MathWorks 的网站声称 Polyspace 使用形式数学来验证程序的属性。有免费试用版，但不适用于家庭用户。有谁知道 Polyspace 是否拥有或使用数学理论库来正式验证程序的属性？如果是，这个库是用哪种语言编写的？