We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology of the system (e.g.\ pipeline, ring). The logic can be easily embedded in monadic second order logic of finitely many successors, and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.
翻译:我们认为参数化并存系统是由一定数量但未知的元件组成的参数化共生系统,这些元件是复制一套特定的有限状态自动成形系统获得的。各元件通过执行原子相互作用进行交流,其参与者同时更新其状态。我们采用了一种互动逻辑,以具体说明相互作用的类型(例如,共和会议、广播)和系统的地形学(例如,管道、环)。逻辑可以很容易地嵌入为数有限的许多继承者的单数第二顺序逻辑,因此是可以分解的。证明这种参数化系统的安全特性,例如僵局自由或相互排斥,需要推导一种含有所有系统实例所有可达状态的演化变异性,而不是不安全状态。我们从描述相互作用的公式中提出一种直接自动合成变异性的方法,而没有昂贵的固定点的迭代。我们实验证明,这种变性足以核实大量系统的安全特性,包括教科书实例(哲学家、同步计划)、典型的相互排斥算法、缓存-聚合协议和自我稳定算法,作为任意数字。