A Specification and Validation Environment for Distributed Coordination Algorithms

随着网络的扩展，帮助协议和分布式算法原型的软件环境变得越来越重要。需要强大的规范和验证技术。一个基于耦合有限状态机模型的原型环境SPANER被证明对精确描述和验证小的协调问题是有用的。该奖项探索通过扩展扳手系统的规范能力和实现增强系统的分布式版本来开发更强大的开发环境。通过允许动态激活模块、基于约束的规范和多个时基，规范功能正在得到增强。我们的目标是继续能够验证这种安全和活性属性的规格。分布式实施旨在能够在更短的时间内验证更大、更复杂的协议。在这项工作的过程中开发和测试的想法应该对其他研究人员开发的原型环境有用。

Software environments to aid in the prototyping of protocols and distributed algorithms are increasingly important as networking expands. Powerful techniques for specification and validation are needed. A prototyping environment called SPANNER, based on a coupled finite state machine model, was shown to be useful for precisely specifying and validating small coordination problems. This award explores the development of a more powerful development environment by extending the specification capabilities of the SPANNER system and by implementing a distributed version of the enhanced system. The specification capabilities are being enhanced by allowing dynamic activation of modules, constraint-based specifications, and multiple time bases. The goal is to continue to be able to validate such specifications for safety and liveness properties. The distributed implementation is designed to be able to validate larger and more complex protocols in a shorter amount of time. The ideas being developed and tested during the course of this work should be of use to prototyping environments developed by other researchers.