Verification of compartmental epidemiological models using metamorphic testing, model checking and visual analytics

Compartmental models in epidemiology are widely used as a means to model disease spread mechanisms and understand how one can best control the disease in case an outbreak of a widespread epidemic occurs. However, a significant challenge within the community is in the development of approaches that can be used to rigorously verify and validate these models. In this paper, we present an approach to quantify and verify the behavioral properties of compartmental epidemiological models under several common modeling scenarios including: birth/death rates and multi-host/pathogen species. We build a workflow that uses metamorphic testing, novel visualization tools and model checking to gain insights into the functionality of compartmental epidemiological models. Our initial results indicate that metamorphic testing can be used to verify the implementation of these models and provide insights into special conditions where these mathematical models may fail. The visualization front-end allows the end-user to scan through a variety of parameters commonly used in these models to elucidate the conditions under which an epidemic can occur. Furthermore, specifying these models using a process algebra allows one to automatically construct behavioral properties that can be rigorously verified using model checking. Together, our approach allows for detecting implementation errors as well as handling conditions under which compartmental epidemiological models may fail to provide insights into disease spread dynamics.