问题标签 [formal-methods]

我正在从事一个医疗嵌入式系统项目，类似于输液泵。我们有一个初步的原型，我们正在进入项目的第二阶段。在这里，我们希望通过使用形式化方法做得更好。我有 CS 背景，但没有任何正式工具或语言的经验。我发现了一些来自宾夕法尼亚大学和亚利桑那州的出版物，他们在输液泵原型上使用了 Uppaal、AADL 等 ( http://www.fda.gov/medicaldevices/productsandmedicalprocedures/generalhospitaldevicesandsupplies/infusionpumps/ucm202511.htm )。我想向社区询问哪些工具或语言（最好是开源）可用于以下目的。

1) 目前，我们将 UI 屏幕作为状态机，并且有很多状态。是否有正式的工具来指定和嵌入算法以及这些屏幕？Z 或 TLA 可以用于此目的吗？

2) 我应该使用哪些工具和语言来描述软件架构和设计？我们没有 RTOS 或复杂的硬件，它只是微控制器。

3) 建模和验证控制算法和协议状态机的工具。

4) 从规范生成测试用例的工具。

我应该学习不同的语言或工具吗？是否有一套最小的工具可以满足上述要求？

我无法理解如何触发 Lean 对类型类的使用。这是一个小例子的尝试：

关键是我希望 Lean 看到它可以使用 HA 从引理 T 中推断出 toto A。我错过了什么？

给定一个系统及其完整的状态空间，我可以说该状态空间是该系统行为的正式规范吗？

我在这里更清楚地改变了我的问题。有两种不同的模型，一种是发送者模型，一种是接收者模型。我想检查发送的消息与接收者接收的消息不同的属性。

LTLSPEC (G(state=receiver -> messageTransmited != messageReceived))

我在ProB中可视化大量代码时遇到问题。此图显示了带有（使用 Graphviz dotty）ProB 的服务器的登录部分，但没有解决大量代码获取该图的解决方案。请让我知道您的建议和想法，

合金新手在这里。

我真的很喜欢在 Alloy 中创建约束并让分析器根据约束检查模型是否有效。

但我问自己，“这些约束定义仅仅是心理体操，还是有助于构建更好的软件？”</p>

让我们举一个具体的例子。在电子邮件客户端地址簿的模型中，可以定义此约束以将新条目添加到地址簿中：

新书 b' 中的地址映射与旧书 b 中的地址映射相同，但增加了从名称到地址的链接。该约束在合金中表示为： b'.addr = b.addr + n->a

那个好漂亮。

但是当在代码中实现添加操作时，我很难看到它的相关性。例如，我在 Common Lisp 中实现了add操作：

用文字来说：“这是一个名为add的函数的定义，它具有三个参数：b、n和a（书、姓名、地址）。使用 Common Lisp 集合函数adjoin将列表 ( na ) 添加到b。”</p>

该函数似乎正确地实现了一个简单的添加函数。我如何处理我在 Alloy 中定义的约束？我应该编写额外的代码来表达约束吗？在伪代码中：[1]

编写这样的代码似乎需要做很多工作，而且没有明显的好处。

所以我的问题是：在代码中实现合金模型时，我应该如何处理合金中定义的约束？

此外，是否有描述如何将合金模型转换为代码的教程，包括如何在代码中使用合金约束定义的描述？

谢谢你。

[1] 注意：我意识到 Common Lisp 中有一个名为 Screamer 的语言扩展，用于约束编程

我有以下简单的证明：

在证明状态下，伊莎贝尔说：

成功尝试通过导出规则解决目标：n * n < a * b

但是之后：

无法应用初始证明方法⌂：使用此方法：n < a n < b 目标（1 个子目标）：1. n * n < a * b

问题是什么？。实际上，我对完成专业的实际单个步骤感兴趣，所以我认为伊莎贝尔可以告诉我方法。

我在 UPPAAL 中模拟了两个触发器的定时模型，当我尝试验证一些属性时，我达到了 6M 状态并且我的笔记本电脑内存不足，消耗了大约 5Go，谁能告诉它是 UPPAAL 可以的近似状态数处理 ？以及在 UPPAAL 中处理状态爆炸的可能技术是什么？
谢谢

有时在 UPPAAL 中，我发现了一个整数变量的示例，它采用两个值，例如 int x:=1-0，这到底是什么意思？像 x 先取“1”然后取“0”还是 X 只是两个值的数组？

谢谢

在阅读 lambda 演算的正式描述时，变量集似乎总是被定义为可数无穷大。为什么这个集合不能是有限的似乎很清楚；将变量集定义为有限会以不可接受的方式限制术语构造。但是，为什么不允许集合是不可数无限的呢？

目前，我收到的对这个问题的最明智的回答是，选择可数无限的变量集意味着我们可以枚举变量，从而自然地描述如何选择新变量，比如 alpha 重写。

我正在寻找这个问题的明确答案。