Formally Reasoning About and Automatically Generating Sequential and Parallel Simulations

This 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.