The 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.

In time warp simulations, the overheads associated with rollbacks, state-saving and the communication induced by rollbacks are the chief contributors to the cost of the simulation; thus, these aspects of the simulation have been primary targets for optimizations. Unfortunately, the behavior of the time warp simulation is highly dynamic and greatly influenced by the application being simulated. Thus, the suggested optimizations are only effective for certain intervals of the simulation. This paper argues that the performance of time warp simulators benefits from a dynamic on-line decision process that selects and configures the sub-algorithms implementing the different aspects of the simulator to best match the current behavior of the simulation. In particular we study control strategies to dynamically: (i) adjust the checkpointing (or state-saving) interval (ii) select the cancellation strategy (lazy or aggressive), and (iii) determine the policy for aggregating the application messages (an optimization that significantly improves the performance in message passing environments). The strategies have been implemented in the WARPED time warp simulation kernel and the performance obtained via the dynamically controlled optimizations is shown to surpass that of their best performing static counterparts.