Information Technology Reference
In-Depth Information
Runtime Verification
and Refutation for Biological Systems
Hillel Kugler
Microsoft Research, Cambridge UK
hkugler@microsoft.com
Abstract.
Advanced computational models are transforming the way
research is done in biology, by providing quantitative means to assess the
validity of theories and hypotheses and allowing predictive capabilities,
raising an urgent need to be able to systematically and eciently analyze
runtime properties of models. In this tutorial I describe key biological
applications, modeling formalisms, property specification languages, and
computational tools utilized in this domain, survey the techniques and
research from the formal verification, machine learning and simulation
communities that are currently being used, and outline opportunities for
the runtime verification community to contribute new scalable methods.
1 Introduction
Understanding how biological and ecological systems develop and function re-
mains one of the main open scientific challenges of our times, and is key towards
developing treatments for disease, helping conserve biodiversity and addressing
global environmental challenges . Computational models are becoming increas-
ingly important in biology and ecology, as a way to formulate hypotheses, as-
sumptions and mechanisms and quantitatively assess whether a theory explains
the known data, and make new predictions. As the utility of computational mod-
els grows in the biological sciences, it is becoming critical to be able to eciently
test whether a biological model explains known data, what assertions and tem-
poral properties hold for a model, and which initial conditions and environment
inputs can lead to a specific desired outcome.
Techniques from runtime verification have the potential to be adapted and
utilized to address these challenges, especially since many of the biological mod-
els are very complex, and therefore a pure testing approach can easily fail to
identify important model behavior, whereas formal verification methods do not
scale to many of the real-world models. In this tutorial I will survey the state
of the art biological research with significant modeling components in areas of
developmental biology, immunology, stem cells, DNA computing and global eco-
logical studies, focusing on the challenges related to run time verification and
and model refutation.
