Formal Verification of Nonlinear Biological Systems.

摘要

Abstraction and composition have proved to be particularly useful in extending the reach of formal verification. Abstraction reduces the size of the system under investigation by neglecting details irrelevant to the properties of interest. Compositionality allows us to decompose large-scale system into smaller components and verify each component individually and reason about the verification of entire system from verified components. Together, these two techniques permit us to substitute a component with its equivalent abstraction such that the overall system retains the property of interest.;In this thesis, we first show that in the context of the Iyer et al. (IMW) 67-variable cardiac myocycte model, it is possible to replace the detailed 13-state probabilistic model of the sodium channel dynamics with a much simpler Hodgkin-Huxley (HH)-like two-state model, while only incurring a bounded approximation error. We then extend our technique to the 10-state model of the fast recovering calcium-independent potassium channel. The basis of our results is the construction of an approximate bisimulation between the HH-type abstraction and the corresponding detailed ion channel model, both of which are input-controlled (voltage in this case) CTMCs.;We then present BFComp, an automated framework based on Sum-Of-Squares (SOS) optimization and delta-decidability over the reals to compute Bisimulation Functions (BF). BF formalizes the notion of abstraction in dynamical systems by establishing approximate equivalence between the original system and its abstract equivalent. In addition, BFComp framework supports compositional reasoning. In this work, we are particularly interested in feedback composition, where output of one component is the input to another, and vice versa. By appealing to small-gain theorem of BFs, it can be shown that an abstract component with lower complexity can replace a detailed component in a feedback composition. Such substitution is safe in the sense that approximation error between the detailed and abstract component will not be amplified in the feedback composition. We will illustrate the utility of BFComp on a canonical cardiac-cell model, showing that the four-variable Markovian model for the slowly activating potassium current component can be safely replaced by a one-variable Hodgkin-Huxley-type approximation.;Finally, we present what we believe to be the first formal verification of a biologically realistic (nonlinear ODE) model of a neural circuit in a multicellular organism: Tap Withdrawal (TW) in C. Elegans, the common roundworm. TW is a reflexive behavior exhibited by C. Elegans in response to vibrating the surface on which it is moving; the neural circuit underlying this response is the subject of this investigation. Specially, we perform reach-tube-based reachability analysis on the TW circuit model of Wicks et al. (1996) to estimate key model parameters. Underlying our approach is the use of Fan and Mitra's recently developed technique for automatically computing local discrepancy (convergence and divergence rates) of general nonlinear systems.;The results we obtain are a significant extension of those of Wicks et al. (1996), who equip their model with fixed parameter values that reproduce the predominant TW response they observed experimentally in a population of 590 worms. In contrast, our techniques allow us to much more fully explore the model's parameter space, identifying in the process the parameter ranges responsible for the predominant behavior as well as the non-dominant ones. The verification framework we developed to conduct this analysis is model-agnostic, and can thus be re-used on other complex nonlinear systems.