并发系统建模工具

Question

我目前正在参加并行软件设计课程，并且我们非常关注建模。我看到了这方面的价值，但我不确定我们使用的工具是可怕的，好的还是介于两者之间的，因为我找不到任何其他示例。我们目前正在使用LTS分析仪，并提供更多信息here。

所以我的问题是，对于已经完成并发系统设计的任何人，是否在实现之前为应用程序建模？如果有的话，您使用了哪些工具？谢谢。

Answer 1

虽然我没有用过自己，但我已经听说了一些关于JPF的好东西（计划尽快使用它）。

Answer 2

一个在各行业并行/分布式系统的建模&验证更广为人知的工具是SPIN模型检测：http://spinroot.com/spin/ 但是请记住，无论多么正确的设计和/或验证你的模型是，你的实现仍然需要效仿。这是许多项目以这种或那种方式失败的地方。