2011 | OriginalPaper | Buchkapitel
Efficient Scenario Verification for Hybrid Automata
verfasst von : Alessandro Cimatti, Sergio Mover, Stefano Tonetta
Erschienen in: Computer Aided Verification
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
Hybrid Automata (HAs) are a clean modeling framework for systems with discrete and continuous dynamics. Many systems are structured into components, and can be modeled as networks of communicating HAs. Message Sequence Charts (MSCs) are a consolidated language to describe desired behaviors of a network of interacting components and have been extended in numerous ways. The construction of traces witnessing such behaviors for a given system is an important part of the validation. However, specialized tools to solve this problem are missing. The standard approach encodes the constraints in a temporal logic formula or in additional automata, and then use an off the shelf model checker to find witnesses. However, these approaches are too generic and often turn out to be inefficient.
In this paper, we propose a specialized algorithm to find the behaviors of a given network of HAs that satisfies a given scenario. The approach is based on SMT-based bounded model checking. On one side, we construct an encoding which exploits the events of the scenario and enables the incremental use of the SMT solver. On the other side we simplify the encoding with invariants discovered applying discrete model checking on an abstraction of the HAs. The experimental results demonstrate the potential of the approach.