Publikation:

Runtime Verification for Hybrid Analysis Tools

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2015

Autor:innen

Nguyen, Luan Viet
Bogomolov, Sergiy
Johnson, Taylor T.

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-319-23820-3_19
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

BARTOCCI, Ezio, ed., Rupak MAJUMDAR, ed.. Runtime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, proceedings. Cham: Springer, 2015, pp. 281-286. Lecture Notes in Computer Science. 9333. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-23819-7. Available under: doi: 10.1007/978-3-319-23820-3_19

Zusammenfassung

In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Runtime Verification, SpaceEx, dReach, Hybrid Automata, Model-based Development Environment

Konferenz

6th International Conference on Runtime Verification, RV 2015, 22. Sept. 2015 - 25. Sept. 2015, Wien
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690NGUYEN, Luan Viet, Christian SCHILLING, Sergiy BOGOMOLOV, Taylor T. JOHNSON, 2015. Runtime Verification for Hybrid Analysis Tools. 6th International Conference on Runtime Verification, RV 2015. Wien, 22. Sept. 2015 - 25. Sept. 2015. In: BARTOCCI, Ezio, ed., Rupak MAJUMDAR, ed.. Runtime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, proceedings. Cham: Springer, 2015, pp. 281-286. Lecture Notes in Computer Science. 9333. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-23819-7. Available under: doi: 10.1007/978-3-319-23820-3_19
BibTex
@inproceedings{Nguyen2015Runti-52501,
  year={2015},
  doi={10.1007/978-3-319-23820-3_19},
  title={Runtime Verification for Hybrid Analysis Tools},
  number={9333},
  isbn={978-3-319-23819-7},
  issn={0302-9743},
  publisher={Springer},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Runtime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, proceedings},
  pages={281--286},
  editor={Bartocci, Ezio and Majumdar, Rupak},
  author={Nguyen, Luan Viet and Schilling, Christian and Bogomolov, Sergiy and Johnson, Taylor T.}
}
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/52501">
    <dc:creator>Johnson, Taylor T.</dc:creator>
    <dcterms:issued>2015</dcterms:issued>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:language>eng</dc:language>
    <dc:creator>Bogomolov, Sergiy</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Nguyen, Luan Viet</dc:contributor>
    <dcterms:title>Runtime Verification for Hybrid Analysis Tools</dcterms:title>
    <dc:creator>Nguyen, Luan Viet</dc:creator>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52501"/>
    <dc:contributor>Johnson, Taylor T.</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-19T14:13:01Z</dcterms:available>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:abstract xml:lang="eng">In this paper, we present the first steps toward a runtime verification framework for monitoring hybrid and cyber-physical systems (CPS) development tools based on randomized differential testing. The development tools include hybrid systems reachability analysis tools, model-based development environments like Simulink/Stateflow (SLSF), etc. First, hybrid automaton models are randomly generated. Next, these hybrid automaton models are translated to a number of different tools (currently, SpaceEx, dReach, Flow*, HyCreate, and the MathWorks’ Simulink/Stateflow) using the HyST source transformation and translation tool. Then, the hybrid automaton models are executed in the different tools and their outputs are parsed. The final step is the differential comparison: the outputs of the different tools are compared. If the results do not agree (in the sense that an analysis or verification result from one tool does not match that of another tool, ignoring timeouts, etc.), a candidate bug is flagged and the model is saved for future analysis by the user. The process then repeats and the monitoring continues until the user terminates the process. We present preliminary results that have been useful in identifying a few bugs in the analysis methods of different development tools, and in an earlier version of HyST.</dcterms:abstract>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-19T14:13:01Z</dc:date>
    <dc:contributor>Bogomolov, Sergiy</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Schilling, Christian</dc:creator>
    <dc:contributor>Schilling, Christian</dc:contributor>
  </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