Scalable reaction network modeling with automatic validation of consistency in Event-B.

Constructing a large biological model is a difficult, error-prone process. Small errors in writing a part of the model cascade to the system level and their sources are difficult to trace back. In this paper we extend a recent approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to validate for model consistency step-by-step in an automated way. We demonstrate this approach on a model of the heat shock response in eukaryotes and its scalability on a model of the [Formula: see text] signaling pathway. All consistency properties of the model were proved automatically with computer support.

Refinement-based modeling of the ErbB signaling pathway.

The construction of large scale biological models is a laborious task, which is often addressed by adopting iterative routines for model augmentation, adding certain details to an initial high level abstraction of the biological phenomenon of interest. Refitting a model at every step of its development is time consuming and computationally intensive. The concept of model refinement brings about an effective alternative by providing adequate parameter values that ensure the preservation of its quantitative fit at every refinement step. We demonstrate this approach by constructing the largest-ever refinement-based biomodel, consisting of 421 species and 928 reactions. We start from an already fit, relatively small literature model whose consistency we check formally. We then construct the final model through an algorithmic step-by-step refinement procedure that ensures the preservation of the model's fit.

Stepwise construction of a metabolic network in Event-B: The heat shock response.

There is a high interest in constructing large, detailed computational models for biological processes. This is often done by putting together existing submodels and adding to them extra details/knowledge. The result of such approaches is usually a model that can only answer questions on a very specific level of detail, and thus, ultimately, is of limited use. We focus instead on an approach to systematically add details to a model, with formal verification of its consistency at each step. In this way, one obtains a set of reusable models, at different levels of abstraction, to be used for different purposes depending on the question to address. We demonstrate this approach using Event-B, a computational framework introduced to develop formal specifications of distributed software systems. We first describe how to model generic metabolic networks in Event-B. Then, we apply this method for modeling the biological heat shock response in eukaryotic cells, using Event-B refinement techniques. The advantage of using Event-B consists in having refinement as an intrinsic feature; this provides as a final result not only a correct model, but a chain of models automatically linked by refinement, each of which is provably correct and reusable. This is a proof-of-concept that refinement in Event-B is suitable for biomodeling, serving for mastering biological complexity.