HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models


Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson

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.

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

Output Formats Supported (with necessary transformations to preserve semantics)

Planned Output Formats to be Supported in Next Versions

Adding a new output format, especially if there are few semantics mismatches between SpaceEx's networks of hybrid automata (as compositions of base components in network components) takes a few hours to a few days of development time, and effectively amounts to writing a pretty printer and potentially some small transformation passes to preserve semantics (or in many cases, simply handle syntax requirements). Obviously sometimes an output format is incompatible with the input format (e.g., if a tool only supports timed or linear dynamics, but the input model has say nonlinear dynamics). In such cases, we either perform a transformation pass (as specified by the user) or return an error. For example, for a system with nonlinear dynamics, we may try to hybridize the system so that it may be supported by tools that allow only linear dynamics. As more transformation passes are added, more output formats can be supported (for example, if we supported a transformation of initialized rectangular hybrid automata to multirate timed automata or pure timed automata).

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 Downloads

HSCC 2015 Tool Paper (pdf)

Download HyST v1.17, 2015-04-11 (zip)



Benchmarks

Benchmark Examples in Hyst Repository
Nonlinear Reachability Examples for ARCH 2015 (zip)
Large Scale Linear Benchmarks for Reachability (DEDS 2017)
Nonlinear Benchmarks for Invariant Synthesis (ARCH 2016)


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.

Publications