alloy - 如何使用Alloy查找软件架构中的故障

Question

我在学习 Alloy 时获得了很多乐趣，并且很高兴将它应用到我正在从事的一些软件项目中。

过去，我曾非正式地使用轻量级形式化方法(如果是的话)，以一阶逻辑编写我期望系统具有的一些不变量。我从来没有用它来发现缺陷，只是将我的设计和测试集中在关键的属性上。

我现在想超越这一点，并实际使用 Alloy 来查找架构中的故障。我怎样才能做到这一点？我一直采取的方法是:

将架构剥离到一些内核(例如，删除使用集而不是更复杂的数据结构，使用 sig 而不是更详细的枚举)

将不变量编码为 assert

check和 run

然而，虽然学习了很多关于 Alloy 的知识，但这并没有帮助我改进我的架构。在简化我的模型的过程中，我编码的不变量似乎被相应地简化了，并且自然成立。

例如，架构中有一个错误，我们仅通过原型(prototype)设计和测试才遇到。该错误与假设我们是否有 n 有关。序列中的项目，我们可以将它们分成 m 组并按顺序处理每个 m 组。 ( n 恰好比 m 大得多。)问题当然是 m不一定除 n ，因此最后一组可能太小了。这是 设计级缺陷完全可以用逻辑表达，正是为 设计的缺陷类型.然而，我的合金模型没有找到它。它只是简单地抽象出整数大小(请参阅 Why does Alloy tell me that 3 >= 10? 中给出的建议以避免使用数字)，将 n 划分为不相交的组，并且运行良好。

换句话说，似乎 为了确保您的模型包含足够的细节来捕捉缺陷，您几乎需要提前了解缺陷 .

那么，您如何使用 Alloy 来审查软件架构？

PS 我知道在很多情况下你没有这个问题。例如，在查看分布式系统的规范并希望显示不变量时。我的挑战是应用 Alloy 来帮助实现，而不是审查协议(protocol)或规范或状态机或其他逻辑结构。

Answer 1

合金不是最适合推理数字或字符串。
因此，您的模型通常无法检测到与给定字符串的格式或给定整数字段的值相关的错误。

现在，Alloy 最擅长的是推理关系以及对这些关系的约束。
检查断言是向自己保证给定属性成立的一种方法，所以你是对的，仅使用这种技术，你可能会觉得你需要提前了解缺陷。

因此，我更喜欢这种方法，使用运行命令，它只是为您提供一堆满足模型约束的实例。
在这里，您将自行检查生成的一系列实例是否在您正在建模的上下文中“有意义”。您可能会看到您的某些约束过于严格或不够严格，从而使您可以增强您的模型。