HYST: A source transformation and translation tool for hybrid automaton models

Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

62 Citations (Scopus)

Abstract

A number of powerful and scalable hybrid systems model checkers have recently emerged. Although all of them honor roughly the same hybrid systems semantics, they have drastically different model description languages. This situation (a) makes it difficult to quickly evaluate a specific hybrid automaton model using the different tools, (b) obstructs comparisons of reachability approaches, and (c) impedes the widespread application of research results that perform model modification and could benefit many of the tools. In this paper, we present Hyst, a Hybrid Source Transformer. Hyst is a source-to-source translation tool, currently taking input in the SpaceEx model format, and translating to the formats of HyCreate, Flow∗, or dReach. Internally, the tool supports generic model-to-model transformation passes that serve to both ease the translation and potentially improve reachability results for the supported tools. Although these model transformation passes could be implemented within each tool, the Hyst approach provides a single place for model modification, generating modified input sources for the unmodified target tools. Our evaluation demonstrates Hyst is capable of automatically translating benchmarks in several classes (including affine and nonlinear hybrid automata) to the input formats of several tools. Additionally, we illustrate a general model transformation pass based on pseudo-invariants implemented in Hyst that illustrates the reachability improvement.

Original languageEnglish
Title of host publicationProceedings of the 18th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control, HSCC 2015
PublisherAssociation for Computing Machinery
Pages128-133
Number of pages6
ISBN (Electronic)9781450334334
DOIs
Publication statusPublished - 14 Apr 2015
Externally publishedYes
Event18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015 - Seattle, United States
Duration: 14 Apr 201516 Apr 2015

Publication series

NameProceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015

Conference

Conference18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015
Country/TerritoryUnited States
CitySeattle
Period14/04/1516/04/15

Fingerprint

Dive into the research topics of 'HYST: A source transformation and translation tool for hybrid automaton models'. Together they form a unique fingerprint.

Cite this