SHF: CSR: Small: Bounded Verification and Bounded Synthesis

点击翻译按钮获取中文摘要

A common feature of many modern human-engineered systems, such as medical devices, automobiles and aerospace vehicles, is that they involve interaction between discrete software systems and continuous physical systems. Several such systems are safety critical and failures can be catastrophic. How to guarantee that these systems are designed and built correctly? Traditional approaches based on testing need to be supplemented with approaches based on formal methods. Unfortunately, formal verification is an intractable problem in general and, hence, no single formal verification approach can uniformly perform well. This project develops a new approach for formal verification that complements existing approaches. Having a suite of formal verification tools can help find errors earlier in the design cycle to reduce overall development cost and increase assurance of designed complex cyber-physical systems. This project contributes to the existing formal verification technology by developing a new approach for formal verification, called bounded verification. Bounded verification verifies a system by performing a bounded search for a witness that would establish the property. Depending on the property, a witness is a Lyapunov function, an inductive invariant, a controlled invariant and so on. Search for a witness is cast as satisfiability of a quantified (\exists\forall) formula. Satisfiability is decided using a combination of techniques including counterexample guided inductive reasoning, compositional reasoning, simulations, and fixpoint computations. Witnesses generated by bounded verification of the design are used to bootstrap formal verification of the implementation. This project also extends the bounded verification approach to performing automated synthesis of systems. Bounded verification explicitly provides witnesses for correctness, which can be used to aid in the certification process. This project also introduces new links for interaction between the fields of theorem proving and formal verification that aim to foster collaboration and promote progress in both areas.