| Simulation Model Development
and Analysis in UNITY
December 2000
Ernest H. Page, The MITRE Corporation
Marc Abrams, Department of Computer Science, Virginia Tech
ABSTRACT
We evaluate UNITY—a computational model, specification language and
proof system defined by Chandy and Misra [5] for the development of
parallel and distributed programs—as a platform for simulation model
specification and analysis. We describe a UNITY-based methodology for
the construction, analysis and execution of simulation models. The methodology
starts with a simulation model specification in the form of a set of
coupled state transition systems. Mechanical methods for mapping the
transition systems first into a set of formal assertions, permitting
formal verification of the transition systems, and second into an executable
program are described. The methodology provides a means to independently
verify the correctness of the transition systems: one can specify properties
formally that the model should obey and prove them as theorems using
the formal specification. The methodology is illustrated through generation
of a simulation program solving the machine interference problem using
the Time Warp protocol on a distributed memory parallel architecture.
Additional Search Keywords
Parallel simulation, model specification, automated verification
|
