Techniques similar to those used by Intel to debug the floating-point unit in its processors are now being applied to models of human cells in an attempt to better understand how they work. The approach has already led to the development of a safer heart defibrillation technique that slashes the energy needed by a factor of ten.
Speaking at the Alan Turing Centenary Conference in Manchester (Sunday 24 June), Professor Edmund Clarke of Carnegie-Mellon University's Computer Science Department revealed that he plans to use formal techniques to analyse models of the repair mechanism – known as Vp53’ – used by living cells.
“P53 has been called the guardian of the genome,” Clarke said. The p53 signalling pathway tells the cell to either repair its DNA or, if the damage has gone too far, kill itself. The kill signal fails in cancerous cells. Understanding p53’s behaviour better could yield more effective cancer treatments but the models are large and complex which makes it difficult to determine the causes of failure using just computer simulation. Formal analysis, said Clarke, would make it possible “to make predictions from the models that biologists could then verify experimentally”.
The formal verification technique known as ‘model checking’, of which Clarke was a co-inventor, is now used routinely in the design of integrated circuits to overcome a similar problem. Intel started using model checking to verify that the floating-point units, among others, within its chips work as specified in the wake of the company shipping Pentium II processors that had a faulty divide instruction.
The error cost Intel an estimated $500m because it had not been found before shipping despite running billions of test cases in simulation – the number of possible states in a floating-point far exceeds that number of test cases.
Biological processes such as the p53 signalling system are tougher to deal with than digital logic circuits because, Clarke said, “they involve both discrete transitions and continuous changes described by differential equations. These things are very difficult to analyse”.
Work so far has yielded results. In the defibrillation study, a team that included researchers from CMU, Cornell University, NYU and Stony Brook performed what they claim was the first automated formal analysis of a realistic model of a cardiac cell. The formal model made it possible to find the ranges of values in the model that led to the states under which hearts tend to go into ventricular fibrillation without the need to perform exhaustive simulation.
A similar study into pancreatic cancer found 12 genes that are present in patients who survive pancreatic cancer. Clarke said he is looking for biologists to help with the formal analysis of the p53 signalling pathway. “The proper mode is to find a biologist who wants to collaborate with you. We need to know things such as reaction rates, so you need to work with a biologist who has experience of how those biochemical reactions proceed,” he explained.