Synthesizing Finite-State Protocols from Scenarios and Requirements
Synthesizing Finite-State Protocols from Scenarios and Requirements
复制标题
根据场景和要求综合有限状态协议
DOI：
10.1007/978-3-319-13338-6_7
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Abhishek Udupa
中科院分区：
文献类型：
--
作者：
R. Alur;Milo M. K. Martin;Mukund Raghothaman;C. Stergiou;S. Tripakis;Abhishek Udupa
场景或消息序列图提供了一种直观的方式来描述分布式协议所需的行为。在本文中，我们提出了一种用场景来描述和综合有限状态协议的新方法：我们证明了，如果给定的场景充分覆盖了期望实现的所有状态，那么从一组场景中自动派生出一个分布式实现是可能的，该集合增加了一组安全和活性需求。我们首先从给定的场景中推导出不完备的状态机，然后综合对应于完成单个过程的转换关系，从而使全局产品满足指定的要求。一般而言，该完成问题具有与验证问题相同的复杂性PSPACE，但与验证问题不同的是，即使对于恒定数量的过程，该完成问题仍然是困难的(NP-完全)。提出了一种基于反例引导的归纳综合算法来解决完备化问题。我们使用经典的交替比特协议、VI缓存一致性协议和一致性协议来评估所提出的协议描述方法和综合算法的有效性。
Scenarios, or Message Sequence Charts, offer an intuitive way of describing the desired behaviors of a distributed protocol. In this paper we propose a new way of specifying and synthesizing finite-state protocols using scenarios: we show that it is possible to automatically derive a distributed implementation from a set of scenarios augmented with a set of safety and liveness requirements, provided the given scenarios adequately cover all the states of the desired implementation. We first derive incomplete state machines from the given scenarios, and then synthesis corresponds to completing the transition relation of individual processes so that the global product meets the specified requirements. This completion problem, in general, has the same complexity, PSPACE, as the verification problem, but unlike the verification problem, is still hard (NP-complete) even for a constant number of processes. We present an algorithm for solving the completion problem, based on counterexampleguided inductive synthesis. We evaluate the proposed methodology for protocol specification and the effectiveness of the synthesis algorithm using the classical alternating-bit protocol, the VI cache-coherence protocol, and a consensus protocol.