Abstract
As the key step in verifying hybrid systems, the computation of reachable sets largely determines the complexity and thus the applicability of a verification approach. Most existing methods compute the reachable set without considering the specification to be verified. This paper presents an approach that identifies for abstractions of the hybrid model those behaviors that potentially violate the specification. A tailor-made sequence of validation procedures then checks the existence of these behaviors for the original model. In many cases, the proposed iterative algorithm that combines model abstraction, behavior validation, and model refinement to verify the specification explores a considerably smaller part of the reachable set than standard techniques. The paper describes an implementation of the procedure and illustrates the approach for an automotive cruise control example.
Original language | English |
---|---|
Pages (from-to) | 289-294 |
Number of pages | 6 |
Journal | IFAC proceedings volumes |
Volume | 36 |
Issue number | 6 |
DOIs | |
Publication status | Published - Jun 2003 |
Externally published | Yes |
Event | IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2003 - St. Malo, Brittany, France Duration: 16 Jun 2003 → 18 Jun 2003 |
Keywords
- Abstraction
- Counterexample
- Hybrid system
- Model refinement
- Reachability analysis
- Verification