Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
HyComp: An SMT-Based Model Checker for Hybrid Systems
verfasst von : Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
HyComp
is a model checker for hybrid systems based on Satisfiability Modulo Theories (SMT).
HyComp
takes as input networks of hybrid automata specified using the HyDI symbolic language.
HyComp
relies on the encoding of the network into an infinite-state transition system, which can be analyzed using SMT-based verification techniques (e.g. BMC, K-induction, IC3). The tool features specialized encodings of the automata network and can discretize various kinds of dynamics.
HyComp
can verify invariant and LTL properties, and scenario specifications; it can also perform synthesis of parameters ensuring the satisfaction of a given (invariant) property. All these features are provided either through specialized algorithms, as in the case of scenario or LTL verification, or applying off-the-shelf algorithms based on SMT. We describe the tool in terms of functionalities, architecture, and implementation, and we present the results of an experimental evaluation.