HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models
Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson
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.
Input Formats Supported
- SpaceEx XML
- Matlab: We can directly create hybrid automaton models in HyST's interchange format from Matlab. This is accomplished by loading the hyst.jar file into Matlab, then using Matlab's Java interface to instantiate, manipulate, and transform the Java data structures used for the intermediate representation of the hybrid systems models. This lets you, for example, transform or call matrix operations over matrices defining system dynamics (e.g., x' = Ax). In practice, we use this to parameterize and instantiate models using constants (such as circuit element values like resistance, inductance, etc.).
- Java and other languages: If you can load the HyST jar library, probably you can use the internal data structures similar to the Matlab interface
Planned Input Formats to be Supported in Next Versions
- Compositional Interchange Format (CIF) for hybrid systems
Output Formats Supported (with necessary transformations to preserve semantics)
- SpaceEx XML
- HyComp / HyDI (nuXmv)
- MathWorks Simulink / Stateflow (as continuous-time Stateflow charts); extra info on SLSF translation
Planned Output Formats to be Supported in Next Versions
- Ptolemy II: Continuous Time Model of Computation
- We will eventually add output formats for other popular tools, in part based on numbers of requests to support a given tool. If you'd like HyST to support a particular tool, please email us.
If you would like to help in the development or suggest a new output format not already supported, please contact us. The benefit of doing this is you get access to a large repository of benchmarks of various classes (from timed automata to compositions of networks consisting of nonlinear hybrid automata) and can easily benchmark your tool against the other tools HyST already supports. While we would prefer tool developers use standardized interchange formats for their input models like the Compositional Interchange Format (CIF) that evolved from the Hybrid Systems Interchange Format (HSIF), we would be happy to have interested tool developers whose tools have different input formats help us support them in HyST. We are generally less interested to support additional input formats as we hope tool developers will eventually standardize on formats like CIF (especially if the tool is essentially operating on hybrid automata or networks thereof), but we will certainly discuss additional input formats if there is a clear reason (such as modeling stochastic behavior).
Papers and DownloadsHSCC 2015 Tool Paper (pdf)
Download HyST v1.17, 2015-04-11 (zip)
Nonlinear Reachability Examples for ARCH 2015 (zip)
HyST has been tested on both Windows 7/8/10 and Linux (Ubuntu). If you are a tool developer or researcher interested in using or extending HYST to support other tools, we are more than welcome to contributions and collaborations. We currently have a private source code repository on GitHub to which we are happy to invite interested users and developers. We plan to make the repository fully open under an open source license in early 2016.
HyST GitHub Repository
If you need any help using HYST or have suggestions, please feel free to contact any or all of the authors.
HyST began its developement with exlusive support provided by the Air Force Research Laboratory during the summer 2014 Visiting Faculty Research Program (VFRP) at the Information Directorate, in Rome, NY, and built upon a prior open-source project by Christopher Dillo.
- Stanley Bak, Taylor T. Johnson, "Periodically-Scheduled Controller Analysis using Hybrid Systems Reachability and Continuization", In 36th IEEE Real-Time Systems Symposium (RTSS 2015), IEEE Computer Society, San Antonio, Texas, December 2015. This paper presents an abstraction that converts a hybrid automaton to a purely continuous system implemented as a transformation pass in Hyst.
- Hoang-Dung Tran, Luan Viet Nguyen, Taylor T. Johnson, "Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis", In Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2015), Seattle, Washington, April 2015
- Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, "HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models", In 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), ACM, Seattle, Washington, April 2015.