High-level Hybrid Systems Analysis with Hypy

Stanley Bak, Sergiy Bogomolov, Christian Schilling

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    Hybrid systems play an important role in many application domains. A range of powerful analysis methods for this class of systems perform high-level analysis, where, iteratively,(1) a reachability computation is performed on a system model, (2) the result of the analysis is examined, and (3) the model is modified and the process repeats. For example, a well-known high-level analysis method is counter-example guided abstraction refinement (CEGAR), where, at each iteration, the model is refined based on the counter-example produced by the reachability computation. In this paper, we present hypy, a python library which strives to ease the development of high-level analysis approaches. Hypy provides the necessary machinery to run a number of up-to-date hybrid systems analysis tools, parse their outputs, and modify the models. The modi_cations are performed using HyST, a source-to-source model transformation framework, which supports output formats including SpaceEx, Flow*, dReach, and HyCreate. HyST, however, does not run reachability tools nor interpret their output. The developed hypy library fills this gap, providing an extendable and exible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identi_cation, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.
    Original languageEnglish
    Title of host publicationBenchmark for Verification of Fault-Tolerant Clock Synchronization Algorithms
    EditorsG Frehse and M Althoff
    Place of PublicationUSA
    PublisherEasyChair Publications
    Pages80-90pp
    EditionPeer Reviewed
    DOIs
    Publication statusPublished - 2017
    Event3rd International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH 2016) - Vienna, Austria, Australia
    Duration: 1 Jan 2016 → …
    http://www.easychair.org/publications/publication_ethics

    Conference

    Conference3rd International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH 2016)
    Country/TerritoryAustralia
    Period1/01/16 → …
    OtherApril 12 2016
    Internet address

    Fingerprint

    Dive into the research topics of 'High-level Hybrid Systems Analysis with Hypy'. Together they form a unique fingerprint.

    Cite this