Sciweavers

IPPS
1999
IEEE

A Formal Framework for Specifying and Verifying Time Warp Optimizations

13 years 8 months ago
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 ...
Victoria Chernyakhovsky, Peter Frey, Radharamanan
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where IPPS
Authors Victoria Chernyakhovsky, Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry Alexander, Harold W. Carter
Comments (0)