Formal Model Refinement for Complex Biological Systems

Abstract

There is a big interest in building large biological models and various approaches are being used for constructing such systems. Larger models are needed in system-level approaches (such as systems biology, systems medicine, systems immunology, etc.) to describe the global behavior of a complex system as a result of the interactions between myriads of local processes. Mostly it is done by assembling present submodels and then adding more details to these models. Such models are rarely successful in the biological domain, as opposed to software systems engineering where the technique is widely used. The main reason for this is that the interaction between the submodels is not included through their composition and so the resulting model remains to a large extent a heterogeneous collection of separate modules. This also leads to the new model exhibiting poor experimental fit to laboratory data, even if the separate modules were carefully fitted to the relevant local data. Consequently, model fitting has to be (re)done, a process whose computational complexity increases quickly with the size of the model, also one that requires more and more new data to be done successfully. The approach we took in this thesis is to develop a complex model step by step by adding details starting from a “blueprint-like” basic model, making sure that quantitative model properties such as its data fit, are preserved in each extension step. We used Event-B modeling for this purpose. Event-B offers a great feature of refinement which is vital for building large models. In Event-B, a large model is constructed through stepwise refinement. We start with a basic model which has confined details and present further information of the model by adding new events in different refinement steps. The models we get with Event-B refinement are formally connected to each other through the refinement relation and can be employed at any level of details. Event-B comes with the tool support of Rodin which also serves the purpose of formal verification at each step of the model building. To the best of our knowledge, this was the first time Event-B was being used for the modeling of biological systems. We introduce in this thesis a systematic method for building an Event-B model corresponding to a given chemical reaction network, in such a way that mass-conservation relations in the reaction network become invariant properties that can be checked in Event-B. The proof-of-concept demonstration of our method is done on the heat shock response model, a prototype of biological adaptation and response to external stimuli. We demonstrate the scalability of the approach on a model for the ErbB signaling pathway, a key regulatory mechanism in many types of cancer, leading to an Event-B model with almost one thousand events and more than four hundred variables, one of the largest Event-B models ever built. We discuss the scalability of our method and its applicability in systems biology. We also discuss the feasibility of Event-B to capture intricacies of complex systems in a slightly different setup, describing the access of patients in a health care system. This study is also an investigation into the potential of formal methods in decision support, with a focus on system designs that ensure global robustness properties and guaranteed service access.