Safety Verification for Linear Systems

An embedded software controller is safe if the composition of the controller and the plant does not reach any unsafe state starting from legal initial states (in an unbounded time hori-zon). Linear systems – specified using linear ordinary differ-ential or difference equations – form an important class of models for such control systems. We present a new decid-ability result for safety verification of linear systems. Our de-cidability result assumes that the set of initial states and the set of unsafe states satisfy some conditions. When the set of initial and unsafe states do not satisfy these conditions, they can be overapproximated by sets that do satisfy the condi-tions. We thus get a counterexample guided abstraction re-finement (CEGAR) procedure for the unconstrained safety verification of linear systems. Our new procedure performs abstraction-refinement on the initial and unsafe region, and not on the system itself. We present the new procedure and describe experimental results that demonstrate its effective-ness. Categories and Subject Descriptors C.3 [Special-purpose and application-based systems]: Real-time and embedded systems; D.2.4 [Software verifi-cation]: Formal method