Safety Verification Proofs for Physical Systems
Tony Loeser, Yumi Iwasaki, Richard E. Fikes · 1998
While much progress has been made on veri-fication of discrete systems such as computer programs, work on formal verification of con-tinuous, physical systems has been limited. We present a technique for verification of safety properties of such systems. Our algo-rithm 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 trajec-tories comprised of a sequence of qualitative states and state transitions. The applicabil-ity 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.