ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated. If you have any questions, please contact Marianne Reed at .

Show simple item record

dc.contributor.authorFrey, Peter
dc.contributor.authorRadhakrishnan, Radharamanan
dc.contributor.authorCarter, Harold. W.
dc.contributor.authorWilsey, Philip A.
dc.contributor.authorAlexander, Perry
dc.identifier.citationFrey, 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
dc.identifier.otherDigital Object Identifier 10.1109/32.979989
dc.description.abstractThis 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.
dc.subjectFormal specification
dc.subjectFormal verification
dc.subjectTheorem proving
dc.subjectParallel discrete event simulation
dc.subjectTime warp
dc.titleA formal specification and verification framework for Time Warp-based parallel simulation

Files in this item


This item appears in the following Collection(s)

Show simple item record