Hybrid automata : from verification to implementation

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

BAK, Stanley, Omar Ali BEG, Sergiy BOGOMOLOV, Taylor T. JOHNSON, Luan Viet NGUYEN, Christian SCHILLING, 2019. Hybrid automata : from verification to implementation. In: International Journal on Software Tools for Technology Transfer. Springer. 21(1), pp. 87-104. ISSN 1433-2779. eISSN 1433-2787. Available under: doi: 10.1007/s10009-017-0458-1

@article{Bak2019Hybri-52996, title={Hybrid automata : from verification to implementation}, year={2019}, doi={10.1007/s10009-017-0458-1}, number={1}, volume={21}, issn={1433-2779}, journal={International Journal on Software Tools for Technology Transfer}, pages={87--104}, author={Bak, Stanley and Beg, Omar Ali and Bogomolov, Sergiy and Johnson, Taylor T. and Nguyen, Luan Viet and Schilling, Christian} }

<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/rdf/resource/123456789/52996"> <dc:contributor>Bak, Stanley</dc:contributor> <dc:creator>Beg, Omar Ali</dc:creator> <dc:contributor>Johnson, Taylor T.</dc:contributor> <dc:creator>Bogomolov, Sergiy</dc:creator> <dc:contributor>Beg, Omar Ali</dc:contributor> <dc:creator>Schilling, Christian</dc:creator> <dcterms:abstract xml:lang="eng">Hybrid automata are an important formalism for modeling dynamical systems exhibiting mixed discrete–continuous behavior such as control systems and are amenable to formal verification. However, hybrid automata lack expressiveness compared to integrated model-based design frameworks such as the MathWorks’ Simulink/Stateflow (SlSf). In this paper, we propose a technique for correct-by-construction compositional design of cyber-physical systems (CPS) by embedding hybrid automata into SlSf models. Hybrid automata are first verified using verification tools such as SpaceEx and then automatically translated to embed the hybrid automata into SlSf models such that the properties verified are transferred and maintained in the translated SlSf model. The resultant SlSf model can then be used for automatic code generation and deployment to hardware, resulting in an implementation. The approach is implemented in a software tool building on the HyST model transformation tool for hybrid systems. We show the effectiveness of our approach on a CPS case study—a closed-loop buck converter—and validate the overall correct-by-construction methodology: from formal verification to implementation in hardware controlling an actual physical plant.</dcterms:abstract> <dc:contributor>Bogomolov, Sergiy</dc:contributor> <dcterms:title>Hybrid automata : from verification to implementation</dcterms:title> <dc:rights>terms-of-use</dc:rights> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52996"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:issued>2019</dcterms:issued> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-25T09:39:12Z</dc:date> <dc:creator>Bak, Stanley</dc:creator> <dc:creator>Nguyen, Luan Viet</dc:creator> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-25T09:39:12Z</dcterms:available> <dc:creator>Johnson, Taylor T.</dc:creator> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Nguyen, Luan Viet</dc:contributor> <dc:contributor>Schilling, Christian</dc:contributor> <dc:language>eng</dc:language> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account