Safety Verification Proofs for Physical Systems

Reference: Loeser, T.; Iwasaki, Y.; & Fikes, R. Safety Verification Proofs for Physical Systems. Knowledge Systems Laboratory, March, 1998.

Abstract: While much progress has been made in 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 math 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.

Full paper available as ps.

Jump to... [KSL] [SMI] [Reports by Author] [Reports by KSL Number] [Reports by Year]
Send mail to: ksl-info@ksl.stanford.edu to send a message to the maintainer of the KSL Reports.