|Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
We propose a method for verifying persistence of nonlinear hybrid systems. Given some system and an initial set of states, the method can guarantee that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flowpipe computation with deductive reasoning about invariants and is more general than each technique alone.
|Year of Publication
NASA Formal Methods - 9th International Symposium
Moffett Field, CA, USA
|Google Scholar | BibTeX | XML