A formal specification and verification framework for Time Warp-based parallel simulation

View/ Open
Issue Date
2002-01Author
Frey, Peter
Radhakrishnan, Radharamanan
Carter, Harold. W.
Wilsey, Philip A.
Alexander, Perry
Publisher
IEEE COMPUTER SOC
Type
Article
Metadata
Show full item recordAbstract
This paper describes a formal framework developed using the Prototype Verification System (PVS) to model and verify distributed simulation kernels based on the Time Warp paradigm. The intent is to provide a common formal base from which domain specific simulators can be modeled, verified, and developed. PVS constructs are developed to represent basic Time Warp constructs. Correctness conditions for Time Warp simulation are identified describing causal ordering of event processing and correct rollback processing. The PVS theorem prover and type-check condition system are then used to verify all correctness conditions. In addition, the paper discusses the framework's reusability and extensibility properties in support of specification and verification of Time Warp extensions and optimizations.
Collections
Citation
Frey, P; Radhakrishnan, R; Carter, HW; Wilsey, PA; Alexander, P. A formal specification and verification framework for Time Warp-based parallel simulation. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING. January 2002. 28(1) : 58-78
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.