Publikation:

High-level Hybrid Systems Analysis with Hypy

Lade...
Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2017

Autor:innen

Bak, Stanley
Bogomolov, Sergiy

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

FREHSE, Goran, ed., Matthias ALTHOFF, ed.. ARCH16 : 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems. Manchester: easychair, 2017, pp. 80-90. EPiC Series in Computing. 43. ISSN 2398-7340. Available under: doi: 10.29007/4f3d

Zusammenfassung

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 modifications 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 flexible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identification, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

hybrid systems, Hypy, Hyst, parameter identification, pseudo-invariant, reachability, tool, verification

Konferenz

ARCH16. 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, 12. Apr. 2016, Wien
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690BAK, Stanley, Sergiy BOGOMOLOV, Christian SCHILLING, 2017. High-level Hybrid Systems Analysis with Hypy. ARCH16. 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems. Wien, 12. Apr. 2016. In: FREHSE, Goran, ed., Matthias ALTHOFF, ed.. ARCH16 : 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems. Manchester: easychair, 2017, pp. 80-90. EPiC Series in Computing. 43. ISSN 2398-7340. Available under: doi: 10.29007/4f3d
BibTex
@inproceedings{Bak2017Highl-52994,
  year={2017},
  doi={10.29007/4f3d},
  title={High-level Hybrid Systems Analysis with Hypy},
  number={43},
  issn={2398-7340},
  publisher={easychair},
  address={Manchester},
  series={EPiC Series in Computing},
  booktitle={ARCH16 : 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems},
  pages={80--90},
  editor={Frehse, Goran and Althoff, Matthias},
  author={Bak, Stanley and Bogomolov, Sergiy and Schilling, Christian}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/52994">
    <dcterms:title>High-level Hybrid Systems Analysis with Hypy</dcterms:title>
    <dc:language>eng</dc:language>
    <dc:creator>Bak, Stanley</dc:creator>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:rights>terms-of-use</dc:rights>
    <dc:contributor>Bogomolov, Sergiy</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Bogomolov, Sergiy</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-25T09:34:56Z</dc:date>
    <dcterms:abstract xml:lang="eng">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 modifications 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 flexible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identification, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.</dcterms:abstract>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52994"/>
    <dc:creator>Schilling, Christian</dc:creator>
    <dc:contributor>Schilling, Christian</dc:contributor>
    <dcterms:issued>2017</dcterms:issued>
    <dc:contributor>Bak, Stanley</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-25T09:34:56Z</dcterms:available>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen