从场景和需求综合可扩展状态协议
Synthesizing Finite-state Protocols from Scenarios and Requirements
摘要：
场景或消息序列图提供了一种直观的方式来描述分布式协议的期望行为。在本文中，我们提出了一种新的方式，指定有限状态协议使用的情况下：我们表明，它是可以自动地从一组增强了一组安全性和活性要求的情况下，得到一个分布式的实现，提供了足够的情况下\emph{cover}所需的实现的所有状态。我们首先从给定的场景中推导出不完整的状态机，然后合成对应于完成各个过程的转换关系，使全局产品满足指定的要求。这个完成问题，一般来说，具有相同的复杂性，PSPACE，作为验证问题，但不像验证问题，是NP完全的一个常数数量的进程。我们提出了两个算法来解决完成问题，一个是基于启发式搜索在空间中的可能完成和基于OBDD的符号不动点计算的基础上。我们评估所提出的协议规范的方法和使用经典的交替位协议的合成算法的有效性。
英文摘要：
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 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 \emph{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 NP-complete for a constant number of processes. We present two algorithms for solving the completion problem, one based on a heuristic search in the space of possible completions and one based on OBDD-based symbolic fixpoint computation. We evaluate the proposed methodology for protocol specification and the effectiveness of the synthesis algorithms using the classical alternating-bit protocol.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
