我使用Alloy对系统建模。我想通过比较实际系统的具体执行与模型的日志跟踪来检查实现的系统是否与Alloy模型匹配。
我看到的工作方式是:
- 在与Alloy中建模的高级概念相对应的点向已实现的系统添加日志，例如"接待员签到客人g1";
- 将这些预处理成Alloy可以理解的形式
- 把这个给Alloy(或其他工具)，然后说"这个模型承认这个痕迹吗?"(这个问题)
这将在系统的操作日志上运行(如果性能有问题，也可能是子集)，并不断验证系统是否按"规范"运行。
那可能/合理吗?
可能是。
合理的我不太确定。对我来说，Alloy擅长在你的规格中发现未知的未知，即陷阱。
一旦使用Alloy分析对规范进行了万无一失的处理，我认为没有必要用不必要的翻译和分析步骤来妨碍您的程序。这不仅容易出错，而且如果您想要验证的跟踪非常多，您可能还会发现分析器的可伸缩性受到限制……但是，这是可行的。所以如果你想要，当然，去做吧……: -)
我使用Alloy对系统建模。我想通过比较实际系统的具体执行与模型的日志跟踪来检查实现的系统是否与Alloy模型匹配。
是的，我认为这是一点工作，但它应该是可行的。我很有兴趣让它发挥作用。这件事我已经考虑很久了。
Loïc正确地认为Alloy在寻找解决方案方面表现出色，但为了使其易于管理，Alloy必须保持较小的范围。虽然这是事实，但Alloy也是一种规范语言。时间问题只是在寻找解决方案。但是，您所描绘的问题是不同的，您已经在日志中有了解决方案。每个事件指定状态中的一个转换。
如果您熟悉Alloy Evaluator，那么您应该知道，一旦您有了解决方案，您就可以在实例上运行任何Alloy代码。在Alloy内部，有一组完整的类来模拟实例并对其运行Alloy代码。
所以我认为你可以从一个初始实例开始，使用你的日志事件来创建一个辅助实例，然后使用Alloy来验证这是一个有效的转换。这将是非常快的，我不明白为什么这不能处理非常多的对象。当然是成千上万，再加上一点缓存技术，就有几百万了。
我们目前正在努力开发Alloy 6，它将集成Electrum，在那里我们将有完整的时间逻辑，这将使规则更容易表达。
我一直在寻找一个客户很长一段时间，想开发必要的代码来桥合金& &;战壕。如果这能像我认为的那样起作用，这对软件行业来说将是非常有趣的。