A framework for formal automated analysis of simulation experiments using probabilistic model checking

Simulation experiments contribute to scientific discovery due to the degree and extent of reproducibility that simulation systems provide. On the other hand, domain scientists may lack expertise in simulation programming and the use of effective methods for instrumenting, evaluating, and comparing models. By utilizing formal automated verification methods, we aim to improve the process of evaluating model assumptions against evidence, and to facilitate selection of new hypotheses to maximize information gain while reducing information processing requirements. To this end, to evaluate the results of a simulation experiment against expected regularities, a probabilistic model checking system is coupled with a Domain-Specific Language that expresses abstract finite state verification properties. These specification patterns are evaluated against the run-time Discrete-Time-Markov Chain model abstracted from the data obtained through aspect-driven automated instrumentation.