Simulation Model Development and Analysis in UNITY |
| |
Authors: | Ernest H Page and Marc Abrams |
| |
Institution: | (1) The MITRE Corporation, 1820 Dolley Madison Blvd, McLean, VA 22102, USA;(2) Department of Computer Science, Virginia Tech, Blacksburg, VA 24061, USA |
| |
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. |
| |
Keywords: | simulation specification simulation verification parallel simulation protocols UNITY |
本文献已被 SpringerLink 等数据库收录! |
|