Protocol Design and Implementation Using Formal Methods

摘要

The paper reports on a number of formal methods that support correct protocoldesign and implementation. These methods are placed in the framework of a design methodology for distributed systems that was studied and developed within the ESPRIT II Lotosphere project. The paper focuses on design methods for synthesizing protocols by successive application of correctness-preserving LOTOS transformations. The transformational approach is described in some detail and is illustrated with a protocol design example. The paper concludes with some suggestions for relating design methods to milestones in the protocol design and implementation processes.