An invariant of a dynamical system is a region wherein the system remains in any execution. Invariants are useful for analyzing a system. They provide assurance that a complex, possibly safety-critical, system does not ever get into an undesirable, or unsafe, state. The twin tasks of (a) computing an invariant of a system, and (b) checking if a given expression is indeed an invariant -- are both notoriously difficult. In the context of software systems, the concept of an ``inductive invariant'' partly overcomes these two difficulties.
This project performs a systematic exploration of the concept of inductive invariants for continuous dynamical systems and hybrid systems. It builds a constructive theory of inductive invariants that provides computability and complexity results for generating inductive invariants of different forms for such systems. The challenge is to develop scalable techniques for highly nonlinear, nondeterministic, and stochastic systems with unknown parameters. Such systems arise commonly in engineering and science. The approach for invariant discovery is based on reducing the problem to algorithmic problems in symbolic and numeric computation.
As a case study, invariant generation techniques are used to analyze pharmacodynamic and pharmacokinetic models from biomedical literature and verify the safety of medical devices such as insulin pumps. An invariant for an insulin pump would provide bounds for blood glucose concentrations. Invariants are useful for improving reliability of simulation tools. Invariant generation techniques will play a significant role in any fully or partly automated methodology for certifying complex systems.
