Safety Verification Proofs for Physical Systems

Papers 1

While much progress has been made on verification of discrete systems such as computer programs, work on formal verification of continuous, physical systems has been limited. We present a technique for verification of safety properties of such systems. Our algorithm treats safety as a reachability problem, and attempts to prove that a system cannot evolve from an abstract initial state into a state in which the safety condition does not hold. This approach is inspired by qualitative simulation techniques and makes use of trajectories comprised of a sequence of qualitative states and state transitions. The applicability of the technique, however, is not limited to qualitative problems, as we can use any amount of quantitative mathematics in the system description. This paper describes the technique, presents example problems, and discusses its limitations as well as potential for use in device engineering.