**Quantitative model refinement**

Much effort is currently invested in developing larger, more finely-grained computational models in many branches of science, supported by developments in computing infrastructure and by advances in quantitative experimental measuring techniques. This is supported by developments in the computing infrastructure and by advances in quantitative experimental techniques. The main parts of a typical computational biomodeling project are the following:

- Biological model. One first chooses the underlying biological model, including the main variables of interest and the interactions among them. The stress on this level is to capture the main aspects of interest and to ignore the less relevant ones.
- Mathematical model. A mathematical model is associated to the biological model. Regardless of the type of mathematics the model is based on (deterministic or stochastic; continuous or discrete), there are many different ways of building the model, possibly leading to different final results. Modeling principles include mass-action kinetics, Michaelis-Menten enzymatics, Hill kinetics, competitive and non-competitive inhibition, etc.
- Qualitative model checking. The mathematical model is then subject to a qualitative check, including logical consistency, mass conservation relations, elementary modes, etc.
- Model fit. This step involves solving a multi-parametric optimization problem where the unknown numerical values of the model parameters are sought so that the model predictions fit well with the available experimental data.
- Model validation. The model predictions are compared with other available (quantitative and qualitative) experimental data and observations.

We focus in this project on computational techniques allowing the quantitative refinement of a model without altering its numerical fit and validation. Our research addresses two main problems in the design of mathematical models in systems biology: (i) the quantitative fit and validation of a large model is a computationally difficult problem; (ii) changing a model (e.g., adding details to it) implies redoing the work on the numerical fit and validation of the model. Our proposed methodology builds on the expertise gained in computer science in (qualitative) program refinement, extending it in a fundamental way to the realm of quantitative biomodels.