EpiSpec: A formal specification language for parameterized agent-based models against epidemiological ground truth

Building complex computational models of the spread of epidemics is a problem that has seen renewed interest in recent years. Such models are being used for understanding real-time disease evolution prediction and are also proving useful in the prevention, monitoring and control of contagious diseases. There is a pressing need to ensure reliability of epidemiological models since they are widely used in safety-critical applications. In this paper, we present a new spatio-temporal specification language, EpiSpec, for describing detailed properties of agent-based computational epidemiological models. We describe the formal syntax of EpiSpec and demonstrate its use by describing various spatio-temporal properties related to disease evolution, and propose the use of statistical model checking as an algorithmic technique for verification and validation of large computational epidemiological models.