An extensible formal framework for the specification and verification of an optimistic simulation protocol

Parallel and distributed software systems are representative of large scale critical and complex systems that require the application of normal methods. Parallel and distributed software systems are notoriously unreliable because implementors often design and develop such systems without a complete understanding of the problem domain; in addition, the nondeterministic nature of certain parallel and distributed systems make system validation difficult if not impossible. In this paper, the application of normal specification and verification to a class of parallel and distributed software systems is presented. Specifically, the prototype verification system (PVS) is applied to the specification and verification of the time warp protocol, a parallel optimistic discrete event simulation algorithm. The paper discusses how the specification of the time warp protocol can be mechanized within a general-purpose higher-order logic framework like PVS. In addition, the paper presents the extensibility of the specification to address and verify different aspects and optimizations of the basic time warp protocol.