近似线性系统参数验证的结构不变量
Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures
摘要：
我们认为并发系统组成的一个有限的，但数量未知的组件，这是一个给定的有限状态自动机的复制实例。组件通过执行交互进行通信，交互是一组组件的同时原子状态变化。我们指定交互的类型（例如\广播）和拓扑（即\体系结构）（例如，流水线，环）通过一个可判定的交互逻辑，这是嵌入在经典的弱顺序演算的一个继任者（WS1S）。证明这种系统的安全属性，如死锁自由或互斥的正确性，需要推断归纳不变量，包含可达状态集，避免不安全状态。我们的方法直接从描述相互作用的公式中合成这样的不变量，而不需要昂贵的定点迭代。我们应用我们的技术来验证几个教科书的例子，如用餐的哲学家，互斥协议和并发系统的抢占和优先级。
英文摘要：
We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology (i.e.\ architecture) of the system (e.g.\ pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
