HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson: NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems (2020) arXiv
- Tran, Hoang-Dung; Nguyen, Luan Viet; Hamilton, Nathaniel; Xiang, Weiming; Johnson, Taylor T.: Reachability analysis for high-index linear differential algebraic equations (2019)
- Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)
- Tran, Hoang-Dung; Nguyen, Luan Viet; Xiang, Weiming; Johnson, Taylor T.: Order-reduction abstractions for safety verification of high-dimensional linear systems (2017)
- Bak, Stanley; Bogomolov, Sergiy; Henzinger, Thomas A.; Johnson, Taylor T.; Prakash, Pradyot: Scalable static hybridization methods for analysis of nonlinear systems (2016)
- Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.: HYST: a source transformation and translation tool for hybrid automaton models (2015)