Fortunately, the Maude representation bore a close resemblance to a safe Petri net , and there are heuristics for solving the "reachability problem" mentioned above that were very fast in practice. The same computation that took Maude hours could be completed in a fraction of a second, making it possible to explore the EGF network interactively. Furthermore, Petri nets have a nice graphical representation that could be used to display how it was possible to reach a state where proteins A and B are activated at the same time. A paper describing this system was published in 2005. Another paper , examining more theoretical issues, was published in 2006. There is an online demo of an old version of this system. A new version, which has been extensively improved by SRI, can be downloaded from SRI.
"Robustness" is an important topic in systems biology. Biological processes are selected to perform their function in spite of all kinds of noise, failures, and disruptions. One kind of robustness that has not been extensively explored is "timing robustness" - can a cell maintain its phenotype when delays in sub-processes are altered?
The process of cell division (the cell cycle) has many steps, some of which execute in parallel, that must be precisely coordinated. But the timing of reactions in a cell cannot be precise, because of signal noise and environmental factors. So the cell cycle has engineering constraints similar to those of asynchronous circuits, which must function reliably despite uncertainty in signal delays and in the environment. In other words, evolution might design robust asynchronous circuits.
Based on this reasoning, we developed a Boolean model of the key regulators of the Caulobacter cell cycle. Concentrations of proteins were modeled with Boolean values, and combinations of reactions were modeled as Boolean gates with arbitrary output delays. Physical processes such as cytokinesis were modeled as finite-state machines.
We wrote a specification in CTL (a temporal logic) that said that the resulting model progressed through the major milestones of the cell cycle in the correct order, forever, and used the model checker NuSMV to determine whether the specification was met for all possible delays.
The result was that the specification was met in almost all cases. There were only two "hazards", where inopportune timing of reactions could result in a failure of the specification (in both cases, the cell cycle would get "stuck"). In each case, it was possible to add a plausible constraint to the model that one reaction always occured before another. The modified model met the specification.
A paper describing this result has been accepted by "Proceedings of the National Academy of Sciences" and will be published soon.
StepMiner works by fitting a step function to the pattern of expression of each individual gene. The algorithm tries each step position (between consecutive time points), and sets the low and high levels of the step function to minimize the sum-of-squares error from the actual data. The best result is assigned a p-value using an F-statistic.
In longer time courses, StepMiner can also find Boolean signals with two steps, where the second step returns to the original level before the first step.
A paper on StepMiner was published in 2007. Free binaries, source code, and examples are also available.
StepMiner has been used in two other studies at Stanford. In one, we analyzed a gene expression microarray time course of the response of osteosarcoma tumor cells to inactivation and reactivation of an additional MYC oncogene from transgenic mice. To be continued...
Murphi is a description language and automatic formal verification system for the high-level description of finite-state systems, including many protocols and distributed algorithms. We have used the system both as a verification tool and as a platform for studying state reduction methods. Several new methods have been discovered and implemented in Murphi.
We have formally specified and verified the core subset of the PCI bus protocol. This website contains a downloadable specification, information on how the specification was written and tested, and a brief desription of the bugs discovered in the official PCI speicfication through our methodology.
We have applied Predicate Abstraction to a few interesting problems. The web page contains a description of the protocols that we have verified.
Another area of research is using BDDs for verification of protocols described in higher-level programming notation. The main ideas are how to translate the high-level notation into BDDs, and how to eliminate redundant information in the BDD representation for applications where they do not otherwise perform well.
Recently, we have resumed investigation of using BDDs to verify designs in synthesizable HDL (e.g. Verilog or VHDL). In order to contain state explosion problems, we have been looking at new methods to compute reasonably accurate overapproximations (superset) of the reachable state space. The method represents the state space using a collection of BDDs which constrain non-disjoint subsets of the state variables of the system (we call these "overlapping projections"). The results seem to be significantly better than previous approximation schemes, which used required the use of disjoint subsets of the state variables. Allowing even a few overlap bits makes it possible to capture some of the communication and interactions between state machines. Draft to appear here shortly.
SVC is an automatic theorem-prover for a decidable fragment of first-order logic which excludes quantifiers, but includes equality, uninterpreted functions and constants, arrays, records, and bit-vectors, as well as propositional connectives. SVC is a general-purpose tool that is a core component of much of our verification research. In particular, it is a central piece of our micro-processor verification technology. More recently, we have been using it for checking specifications of safety-critical systems. We have also experimented with SVC as an alternative ground decision procedure in the PVS theorem-prover, with promising results.
More details, including an on-line demonstration, are available here.
We have been formally verifying high-level processor descriptions using a symbolic simulator and a decision procedure for a quantifier-free fragment of first-order logic with equality and uninterpreted functions.
Certain protocols are designed to simulate a sequence of atomic transactions. However, because the implementation is distributed, it breaks up each transaction into a sequence of smaller steps. The steps of a single transaction may be executed by different nodes of the distributed system. We have developed a general method, which we call aggregation, for using an automated theorem-prover to verify such transaction-oriented protocols.