Framework for Formal Automated Analysis of Simulation Experiments

Abstract

Simulation experiments are becoming a widely feasible medium for scientific discovery due to the amount of traceability and reproducibility which computing systems are able to provide. These characteristics help to ensure the validity of an experimental process, which in turn gives credibility to the propositions supported therein. Simulations can be as complex as the real-world mechanisms they mimic, so the process of experimentation on a simulation can have an explosive search space. We attempt to minimize some of this complexity by reducing data concerns to a more abstract verification model. Additional experimental complexities are reduced by the inclusion of the goal-hypothesis-experiment framework, which includes a domain-specific language for experiment management. By making use of this framework, a scientist needs only to specify the goal of the experiment and give evidence and hypotheses to be tested against a simulation model. By utilizing formal methods of model verification we may automate the process of testing hypotheses against evidence, and facilitate the selection of new hypotheses to maximize the information gained while using the minimum processing requirements. In this thesis, a probabilistic model checker is used as the formal method of verification, and evidence and hypotheses are specified as a temporal logic specifications.