Specification-guided analysis of hybrid systems using a hierarchy of validation methods

Olaf Stursberg, Ansgar Fehnker, Zhi Han, Bruce H. Krogh

Research output: Contribution to journalConference articleAcademicpeer-review

11 Citations (Scopus)


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 languageEnglish
Pages (from-to)289-294
Number of pages6
JournalIFAC Proceedings Volumes (IFAC-PapersOnline)
Issue number6
Publication statusPublished - 2003
Externally publishedYes
EventIFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2003 - Saint Malo, France
Duration: 16 Jun 200318 Jun 2003


  • Abstraction
  • Counterexample
  • Hybrid system
  • Model refinement
  • Reachability analysis
  • Verification


Dive into the research topics of 'Specification-guided analysis of hybrid systems using a hierarchy of validation methods'. Together they form a unique fingerprint.

Cite this