Technical Report
Formalizing and Verifying TimeWarp with FOCUS
Author(s): Max Breitling
Year: 1997
Number: TUM-I9744
Editor:
CR Classification: D.2.1, F.3.1, I.6.1
CR General Terms: Verification
Keywords: timewarp, simulation, Focus, verification, formal methods
Abstract: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.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@techreport{ TUM-I9744,
author = {Max Breitling},
title = {Formalizing and Verifying TimeWarp with FOCUS},
number = {TUM-I9744},
institution = {Technische Univerit\"at M\"unchen},
year = {1997},
url = {http://www4.informatik.tu-muenchen.de/reports/TUM-I9744.html},
abstract = {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.},
CRClassification = {D.2.1, F.3.1, I.6.1},
CRGenTerms = {Verification}
}
]]>