Hybrid Verification by Exploiting the Environment

Abstract

A method of verifying hybrid systems is given. Such systems involve state components whose values are changed by continuous (physical) processes. The verification method is based on proving that only those executions that satisfy constraints imposed by an environment also satisfy the property of interest. A suitably expressive logic then allows the environment to model state components that are changed by physical processes.