A Formal Framework for Specifying and Verifying Time Warp Optimizations

Parallel and distributed systems are representative of large and complex systems that require the application of formal methods. These systems are often unreliable because implementors design and develop these systems without a complete understanding of the problem domain; in addition, the nondeterministic nature of certain parallel and distributed systems make system validation di cult if not impossible. To address this issue, the application of formal speci cation and veri cation to a class of parallel and distributed software systems is presented in this paper. Speci cally, the Prototype Veri cation System PVS is applied to the speci cation and veri cation of the Time Warp protocol, a distributed optimistic discrete event simulation algorithm. The paper discusses how the speci cation of the Time Warp protocol can be mechanized within a general-purpose higher-order theorem proving framework like PVS. In addition, the paper presents the extensibility of the specication to address and ...

• Type: Conference
• Year: 1999
• Where: IPPS
• Authors: Victoria Chernyakhovsky, Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry Alexander, Harold W. Carter
• Keywords: Cation, Distributed And Parallel Computing, IPPS 1999, Time Warp Protocol, Veri Cation