Abrams, MarcPage, Ernest H.2013-06-192013-06-191992http://hdl.handle.net/10919/19804This paper proposes a methodology to automate the construction of simulation programs within the context of a simulation support environment. The methodology starts with a simulation model specification in the form of a set of coupled state transition systems. The paper provides a mechanical method of mapping the transition systems first into a set of formal assertions, permitting formal verification of the transition systems, and second into an executable program. UNITY, a computational model and proof system suitable for development of parallel and distributed programs through step-wise refinement of specifications, is used as the specification and program notation. 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.application/pdfenIn CopyrightTechnical reportTR-92-55http://eprints.cs.vt.edu/archive/00000335/01/TR-92-55.pdf