Runtime Verification for Hybrid Analysis Tools

Kurzanzeige
dc.contributor.authorNguyen, Luan Viet
dc.contributor.authorSchilling, Christian
dc.contributor.authorBogomolov, Sergiy
dc.contributor.authorJohnson, Taylor T.
dc.date.accessioned2021-01-19T14:13:01Z
dc.date.available2021-01-19T14:13:01Z
dc.date.issued2015eng
dc.description.abstractIn 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.eng
dc.description.versionpublishedeng
dc.identifier.doi10.1007/978-3-319-23820-3_19eng
dc.identifier.urihttps://kops.uni-konstanz.de/handle/123456789/52501
dc.language.isoengeng
dc.rightsterms-of-use
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/
dc.subjectRuntime Verification, SpaceEx, dReach, Hybrid Automata, Model-based Development Environmenteng
dc.subject.ddc004eng
dc.titleRuntime Verification for Hybrid Analysis Toolseng
dc.typeINPROCEEDINGSeng
dspace.entity.typePublication
kops.citation.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.}
}
kops.citation.iso690NGUYEN, 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_19deu
kops.citation.iso690NGUYEN, 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, Sep 22, 2015 - Sep 25, 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_19eng
kops.citation.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>
kops.conferencefield6th International Conference on Runtime Verification, RV 2015, 22. Sept. 2015 - 25. Sept. 2015, Wiendeu
kops.date.conferenceEnd2015-09-25eng
kops.date.conferenceStart2015-09-22eng
kops.flag.knbibliographyfalse
kops.location.conferenceWieneng
kops.sourcefieldBARTOCCI, Ezio, ed., Rupak MAJUMDAR, ed.. <i>Runtime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, proceedings</i>. 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_19deu
kops.sourcefield.plainBARTOCCI, 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_19deu
kops.sourcefield.plainBARTOCCI, 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_19eng
kops.title.conference6th International Conference on Runtime Verification, RV 2015eng
relation.isAuthorOfPublicationecb6e671-5807-41bc-bb31-f07a9b7a7c63
relation.isAuthorOfPublication.latestForDiscoveryecb6e671-5807-41bc-bb31-f07a9b7a7c63
source.bibliographicInfo.fromPage281eng
source.bibliographicInfo.seriesNumber9333eng
source.bibliographicInfo.toPage286eng
source.contributor.editorBartocci, Ezio
source.contributor.editorMajumdar, Rupak
source.identifier.eissn1611-3349eng
source.identifier.isbn978-3-319-23819-7eng
source.identifier.issn0302-9743eng
source.publisherSpringereng
source.publisher.locationChameng
source.relation.ispartofseriesLecture Notes in Computer Scienceeng
source.titleRuntime Verification : 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, proceedingseng

Dateien

Sammlungen

Informatik und Informationswissenschaft: Publikationen