从动态规范合成大型动态并发程序
摘要：一个可计算的方法，用于合成具有共享内存模型和常见的硬件可用原语（如原子寄存器、比较和交换、加载链接/存储条件等）的任意大的并发程序。我们合成的程序是动态的：新的进程可以在运行时创建并添加，因此我们的程序通常不是有限状态的。尽管如此，我们成功地利用基于命题时序逻辑的自动合成和模型检查方法。我们的方法在算法上是高效的，其复杂度在任何时候都是与程序的“活动”组件进程数量多项式相关。我们的方法不显式构造所有活动进程的自动机论证产物，从而避免了状态爆炸。相反，对于每对互动的进程，我们的方法构造了一个自动机论证产物（即“对机器”），其中包含这两个进程的所有可能的交互。从每个对机器中，我们可以合成一个正确的“对程序”，根据需要协调这两个相关的进程。我们允许这样的对程序在运行时动态添加。然后，它们与当前活动的对程序“并连组合”，以重新合成增加新对程序后的程序。因此，我们能够在运行时添加新的行为，从而满足新的性质。我们建立了一个“大模型”定理，通过该定理可以证明合成的大程序从对程序继承了正确性属性。
作者：Paul C. Attie
论文ID：0801.1687
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-01-14