A formal specification and verification framework for TimeWarp-based parallel simulation

摘要

The paper describes a formal framework developed using thenPrototype Verification System (PVS) to model and verify distributednsimulation kernels based on the Time Warp paradigm. The intent is tonprovide a common formal base from which domain specific simulators cannbe modeled, verified, and developed. PVS constructs are developed tonrepresent basic Time Warp constructs. Correctness conditions for TimenWarp simulation are identified, describing causal ordering of eventnprocessing and correct rollback processing. The PVS theorem prover andntype-check condition system are then used to verify all correctnessnconditions. In addition, the paper discusses the framework's reusabilitynand extensibility properties in support of specification andnverification of Time Warp extensions and optimizations