-1

我的一位同事编写了一个程序,证明在测试运行多个并发线程的算法试图找到可能触发不需要的条件的序列之后,某些条件将不会被满足。他使用了专为此目的而设计的计算机语言,但我不记得它的名字。为此特定目的提供哪些语言?什么编程语言具有测试并发算法的具体目的?

+0

我找到了源代码我一直在寻找 https://github.com/dgryski/modelchecking/blob/master/spin/ipc.pml,现在我想谷歌“ pml“和”spin“来弄清楚如何编译它。 –

回答

2

Spin是一个流行的开源软件验证工具,由全球数千人使用,由 。该工具可用于对多线程软件应用程序进行正式的 验证。该工具是在贝尔实验室在1980年开始的计算科学研究中心的Unix小组中开发的 。该软件自从1991年以来一直免费提供 ,并且继续发展以跟上新的 的发展。 2002年4月,该工具获得了ACM系统软件奖 。

http://spinroot.com/spin/whatispin.html