Software Verification Meets Biology
The traditional scientific method—every schoolchild learns it: question, hypothesis, experiment, data analysis, and conclusions. Critical to this process are the construction of models whose predictions can be compared to the real universe, and vice-versa. In biology, for example, we deal with models of the mechanisms by which embryonic cells differentiate to become one type of cell in the course of cell division. We want to know whether the absence of a particular protein or gene in the cell determines which type of cell the embryonic cell becomes. The problem is that models of biological systems are so complex that it is difficult to extract useful predications from them.
Is there a way to answer queries about intractably large models of biological systems automatically? This is the problem we set out to solve at Microsoft Research. We have developed an approach called executable biology, which takes advantage of our strength in automatic software proving and formal methods. Executable biology takes analytical tools developed to study reasoning about computer systems and uses them to model and analyze biological systems. Our solution adapts recently discovered automatic-program verification techniques that were originally developed for the analysis of high-performance concurrent software. In particular, we have applied techniques for proving termination of these systems. Many biological models can be viewed as concurrent systems with far more concurrently executing threads than would be found in an average software system. Nonetheless, with some adaptation, the techniques have shown great scalability.
In collaboration with Nir Piterman at the University of Leicester, an expert with unique experience in using formal methods in biological modeling, we are developing an efficient procedure for proving stabilization of biological systems modeled as qualitative networks or genetic regulatory networks. For scalability, our procedure uses modular proof techniques, where state-space exploration is applied only locally to small pieces of the system, rather than the system as a whole. It exploits the observation that, in practice, the form of modular proofs can be restricted to a very limited set. For completeness, our technique falls back on a non-compositional counterexample search.
By using our procedure, we have analysed a number of challenging examples, including a 3-D model of mammalian epidermis and a model of metabolic networks operating in type-2 diabetes. In cases where previous stabilization-proving techniques were known to succeed, our technique attained results far faster, and it obtained new results in cases where tools had previously failed. Biologists can now ask much deeper questions about their models and expect to have tools that automatically answer them. By applying Microsoft Research’s software analysis expertise and tools to a biological scenario, this project is helping to create new business opportunities and partnerships in areas such as biotechnology and healthcare.
Learn more about this research:
- Executable Cell Biology
- The Executable Pathway to Biological Networks
- Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development
- Proving Stabilization of Biological Systems