在某些系统上应用CTL/LTL模型检查

Question

我很抱歉，如果我的标题含糊不清，我正在尝试在Java编写的某些系统上应用CTL/LTL模型检查，但是，我仍然不明白如何使用所述的任何一种方法来达到结果。我是否对我的LTS/编写规范进行建模并使用SPIN之类的工具来验证或？我主要是在寻找一个方向，这将帮助我开始。

再次对不起，但是我在这么多沮丧的情况下寻找了我的问题的解释。

谢谢

Answer 1

我很确定您需要在Promela而不是Java设计系统。然后，您将系统输入Promela中，并在LTL（或CTL）中输入规范，该系统为特定实例输出了模型检查器的C代码。