从场景和需求综合有限状态协议

场景（或消息序列图）提供了一种描述分布式协议期望行为的直观方式。在本文中，我们提出了一种使用场景指定有限状态协议的新方法：我们证明，如果给定场景充分覆盖了期望实现的所有状态，则可以从一组场景加上一组安全性和活性需求自动推导出分布式实现。我们首先从给定场景推导出不完全状态机，然后综合对应于完成各个进程的转移关系，使得全局乘积满足指定的需求。这个完成问题通常具有与验证问题相同的复杂度PSPACE，但与验证问题不同，对于常数个进程它是NP完全的。我们提出了两种解决完成问题的算法：一种基于在可能完成空间中的启发式搜索，另一种基于OBDD符号不动点计算。我们使用经典的交错比特协议评估了所提出的协议规范方法和综合算法的有效性。