Publikation:

Tutorial: Software tools for hybrid systems verification, transformation, and synthesis : C2E2, HyST, and TuLiP

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2016

Autor:innen

Duggirala, Parasara Sridhar
Fan, Chuchu
Potok, Matthew
Qi, Bolun
Mitra, Sayan
Viswanathan, Mahesh
Bak, Stanley
Bogomolov, Sergiy
Johnson, Taylor T.
et al.

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.1109/CCA.2016.7587948
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

2016 IEEE Conference on Control Applications (CCA) : part of 2016 IEEE Multi-Conference on Systems and Control : September 19-22, 2016, Buenos Aires, Argentina. Piscataway, NJ: IEEE, 2016, pp. 1024-1029. ISBN 978-1-5090-0756-1. Available under: doi: 10.1109/CCA.2016.7587948

Zusammenfassung

Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

2016 IEEE Conference on Control Applications (CCA), 19. Sept. 2016 - 22. Sept. 2016, Buenos Aires
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690DUGGIRALA, Parasara Sridhar, Chuchu FAN, Matthew POTOK, Bolun QI, Sayan MITRA, Mahesh VISWANATHAN, Stanley BAK, Sergiy BOGOMOLOV, Taylor T. JOHNSON, Christian SCHILLING, 2016. Tutorial: Software tools for hybrid systems verification, transformation, and synthesis : C2E2, HyST, and TuLiP. 2016 IEEE Conference on Control Applications (CCA). Buenos Aires, 19. Sept. 2016 - 22. Sept. 2016. In: 2016 IEEE Conference on Control Applications (CCA) : part of 2016 IEEE Multi-Conference on Systems and Control : September 19-22, 2016, Buenos Aires, Argentina. Piscataway, NJ: IEEE, 2016, pp. 1024-1029. ISBN 978-1-5090-0756-1. Available under: doi: 10.1109/CCA.2016.7587948
BibTex
@inproceedings{Duggirala2016Tutor-53263,
  year={2016},
  doi={10.1109/CCA.2016.7587948},
  title={Tutorial: Software tools for hybrid systems verification, transformation, and synthesis : C2E2, HyST, and TuLiP},
  isbn={978-1-5090-0756-1},
  publisher={IEEE},
  address={Piscataway, NJ},
  booktitle={2016 IEEE Conference on Control Applications (CCA) : part of 2016 IEEE Multi-Conference on Systems and Control : September 19-22, 2016, Buenos Aires, Argentina},
  pages={1024--1029},
  author={Duggirala, Parasara Sridhar and Fan, Chuchu and Potok, Matthew and Qi, Bolun and Mitra, Sayan and Viswanathan, Mahesh and Bak, Stanley and Bogomolov, Sergiy and Johnson, Taylor T. 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/53263">
    <dc:contributor>Johnson, Taylor T.</dc:contributor>
    <dc:creator>Potok, Matthew</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-03-25T14:20:56Z</dcterms:available>
    <dc:creator>Bogomolov, Sergiy</dc:creator>
    <dc:contributor>Duggirala, Parasara Sridhar</dc:contributor>
    <dc:contributor>Viswanathan, Mahesh</dc:contributor>
    <dc:creator>Johnson, Taylor T.</dc:creator>
    <dc:contributor>Fan, Chuchu</dc:contributor>
    <dc:creator>Fan, Chuchu</dc:creator>
    <dc:creator>Mitra, Sayan</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:abstract xml:lang="eng">Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification.</dcterms:abstract>
    <dcterms:title>Tutorial: Software tools for hybrid systems verification, transformation, and synthesis : C2E2, HyST, and TuLiP</dcterms:title>
    <dcterms:issued>2016</dcterms:issued>
    <dc:language>eng</dc:language>
    <dc:contributor>Bak, Stanley</dc:contributor>
    <dc:contributor>Bogomolov, Sergiy</dc:contributor>
    <dc:contributor>Potok, Matthew</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Mitra, Sayan</dc:contributor>
    <dc:creator>Bak, Stanley</dc:creator>
    <dc:contributor>Schilling, Christian</dc:contributor>
    <dc:contributor>Qi, Bolun</dc:contributor>
    <dc:creator>Viswanathan, Mahesh</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-03-25T14:20:56Z</dc:date>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Qi, Bolun</dc:creator>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/53263"/>
    <dc:creator>Schilling, Christian</dc:creator>
    <dc:creator>Duggirala, Parasara Sridhar</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:rights>terms-of-use</dc:rights>
  </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