Article ID: | iaor20023061 |
Country: | Netherlands |
Volume: | 104 |
Issue: | 1 |
Start Page Number: | 181 |
End Page Number: | 212 |
Publication Date: | Apr 2001 |
Journal: | Annals of Operations Research |
Authors: | Abrams Marc, Page Ernest H. |
We evaluate UNITY – a computational model, specification language and proof system defined by Chandy and Misra 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.