Safety Verification Proofs for Physical Systems

Citation: Tony Loeser and Yumi Iwasaki and Richard Fikes. (1998) Safety Verification Proofs for Physical Systems. In KSL-98-14, March,1998.

Publication techreport ( Edit )
type	Technical Report
bibtype	techreport
Bibtex basics
author	Tony Loeser and Yumi Iwasaki and Richard Fikes
title	Safety Verification Proofs for Physical Systems
number	KSL-98-14
institution	Knowledge Systems, AI Laboratory
year	1998
month	March
Bibtex more
Access Paper
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.

KSL Technical Report ID: KSL-98-14

Abstract	While much progress has been made in verif … 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. s potential for use in device engineering.
Author	Tony Loeser and Yumi Iwasaki and Richard Fikes +
Bibtype	techreport +
Has author	Tony Loeser and Yumi Iwasaki and Richard Fikes +
Has identifier	KSL-98-14 +
Has publishing details	March,1998 +
Has title	Safety Verification Proofs for Physical Systems +
Has where published	KSL-98-14 +
Has year	1998 +
Institution	Knowledge Systems, AI Laboratory +
Ksl tr id	KSL-98-14 +
Month	March +
Number	KSL-98-14 +
Process note	NO +
Title	Safety Verification Proofs for Physical Systems +
Year	1998 +