| |
| Raj Gautam Dutta |
| University of Central Florida, Department of Electrical Engineering & Computer Science |
| 12:00 pm in MSB 318
|
|
|
| Emerging and re-emerging epidemic diseases pose a great
threat to the global population. In the pursuit of understanding the
evolutionary principles that underlie the emergence, spread and
containment of infectious diseases, several complex computational
models have been developed in the area of epidemiology. Identifying
a model that can accurately forecast the outcome of a disease in
various situations and determining the socioeconomic impact of an
inaccurate decision is significantly important. Formal methods have been used to validate the correctness of models in several high-assurance computing areas. We demonstrate the use of high-performance formal methods for the validation of stochastic epidemiological models. We recommend the use of a temporal-logic based probabilistic specification language to describe the expectations of an epidemiological model. The Bayesian SMC then determines the probability with which a given model satisfied the stated formal specification. |