Formalizing and Verifying TimeWarp with FOCUS

The TimeWarp mechanism accomplishes an efficient synchronization between the components of a distributed, discrete event-driven simulator. Using an optimistic simulation strategy, the components of the simulator may calculate ahead locally, sending results to other components without waiting for any events produced by those components, ignoring possible causality problems. In case of an incorrect calculation caused by messages received too late, a component must perform a rollback and cancel some messages already sent, possibly initiating further rollbacks in other components. Nevertheless the distributed TimeWarp algorithm returns a correct result. In this paper this technique is modelled with the development methodology FOCUS and the correctness is formally investigated. Starting from a simple, centralized simulator three development steps are performed, reaching a distributed simulator using TimeWarp. The simulators on various abstraction levels are formally specified, and the development steps are verified using the techniques of FOCUS.     «

The TimeWarp mechanism accomplishes an efficient synchronization between the components of a distributed, discrete event-driven simulator. Using an optimistic simulation strategy, the components of the simulator may calculate ahead locally, sending results to other components without waiting for any events produced by those components, ignoring possible causality problems. In case of an incorrect calculation caused by messages received too late, a component must perform a rollback and cancel som...     »