CSR--EHS: Invariants for Continuous and Hybrid Dynamical Systems

动力系统的不变量是系统保持在任意执行状态的区域。不变量在分析系统时很有用。它们确保一个复杂的、可能对安全至关重要的系统永远不会进入不受欢迎或不安全的状态。(A)计算系统的不变量和(B)检查给定的表达式是否确实是不变量--这两个任务都是出了名的困难。在软件系统的背景下，“归纳不变量”的概念部分地克服了这两个困难。该项目对连续动力系统和混合系统的归纳不变量的概念进行了系统的探索。它建立了归纳不变量的构造性理论，为为这类系统生成不同形式的归纳不变量提供了可计算性和复杂性结果。挑战是为具有未知参数的高度非线性、不确定和随机系统开发可扩展的技术。这样的系统在工程和科学中很常见。不变量发现的方法是基于将问题归结为符号和数值计算中的算法问题。作为一个案例研究，不变量生成技术被用来分析生物医学文献中的药效学和药代动力学模型，并验证诸如胰岛素泵等医疗设备的安全性。胰岛素泵的不变量将提供血糖浓度的界限。不变量对于提高仿真工具的可靠性非常有用。不变量生成技术将在任何全自动化或部分自动化的复杂系统认证方法中发挥重要作用。

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.