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.

• Publication year

  2015

• Venue

  International Conference on Hybrid Systems: Computation and Control

• Publication date

  2015-04-14

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2728606.2728630
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Reducing the wrapping effect in flowpipe construction using pseudo-invariants

  2014influential reference
• Converting Ptolemy II Models to SpaceEx for Applied Verification

  2014cited by this paper
• Parameter synthesis for polynomial biological models

  2014cited by this paper
• Uniform verification of safety for parameterized networks of hybrid automata

  2013cited by this paper
• Satisfiability modulo ODEs

  2013cited by this paper
• Syntax and semantics of the compositional interchange format for hybrid systems

  2013cited by this paper
• Flowpipe approximation and clustering in space-time

  2013cited by this paper
• Flow*: An Analyzer for Non-linear Hybrid Systems

  2013cited by this paper
• Taylor Model Flowpipe Construction for Non-linear Hybrid Systems

  2012cited by this paper
• Formal modeling and validation of Stateflow diagrams

  2012cited by this paper
• δ-Complete Decision Procedures for Satisfiability over the Reals

  2012cited by this paper
• Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion

  2012cited by this paper
• From hybrid data-flow languages to hybrid automata: a complete translation

  2012cited by this paper
• Delta-Decidability over the Reals

  2012cited by this paper
• Appendix to SpaceEx: Scalable Verification of Hybrid Systems

  2011influential reference
• A step towards verification and synthesis from simulink/stateflow models

  2011cited by this paper
• SpaceEx: Scalable Verification of Hybrid Systems

  2011influential reference
• HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction

  2011cited by this paper
• The SMT-LIB Standard Version 2.0

  2010cited by this paper
• Computing reachable states for nonlinear biological models

  2009cited by this paper
• Symbolic analysis for improving simulation coverage of Simulink/Stateflow models

  2008cited by this paper
• Foundations of a Compositional Interchange Format for Hybrid Systems

  2007cited by this paper
• On Taylor Model Based Integration of ODEs

  2007cited by this paper
• Languages and Tools for Hybrid Systems Design

  2006cited by this paper
• Interchange Format for Hybrid Systems: Abstract Semantics

  2006cited by this paper
• The SMT-LIB Standard: Version 1.2

  2005cited by this paper
• PHAVer: algorithmic verification of hybrid systems past HyTech

  2005cited by this paper
• Interchange Formats for Hybrid Systems: Review and Proposal

  2005cited by this paper
• Modeling Techniques, Programming Languages, and Design Toolsets for Hybrid Systems

  2004cited by this paper
• Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations

  2004cited by this paper
• Behavior Based Robotics Using Hybrid Automata

  2000cited by this paper
• Modular Specification of Hybrid Systems in CHARON

  2000cited by this paper
• Vérification et synthèse des systèmes hybrides

  2000cited by this paper
• High-level modeling and analysis of TCAS

  1999cited by this paper
• Theories of Programming Languages: Communicating Sequential Processes

  1998cited by this paper
• The theory of hybrid automata

  1996cited by this paper
• Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems

  1992cited by this paper

• Hybrid dynamical systems modeling of power systems

  2025cites this paper
• A Cegar-centric Bounded Reachability Analysis for Compositional Affine Hybrid Systems

  2025cites this paper
• Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem

  2023cites this paper
• Neural Abstractions

  2023cites this paper
• ARCH-COMP23 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

  2023cites this paper
• On the applicability of hybrid systems safety verification tools from the automotive perspective

  2023cites this paper
• The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems

  2023cites this paper
• Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach

  2022cites this paper
• PDF: Path-Oriented, Derivative-Free Approach for Safety Falsification of Nonlinear and Nondeterministic CPS

  2022cites this paper
• A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output Traces

  2022influential citation
• ARCH-COMP22 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

  2022cites this paper
• A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

  2022cites this paper
• Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL

  2022cites this paper
• Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation

  2022cites this paper
• Verification Approaches for Learning-Enabled Autonomous Cyber–Physical Systems

  2022cites this paper
• Practical End-to-End Verification of Cyber-Physical Systems

  2021cites this paper
• HybridSynchAADL Manual

  2021cites this paper
• ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

  2021cites this paper
• Quantitative Corner Case Feature Analysis of Hybrid Automata with ForFETSMT

  2020cites this paper
• SLEMI: Equivalence Modulo Input (EMI) Based Mutation of CPS Models for Finding Compiler Bugs in Simulink

  2020cites this paper
• NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

  2020cites this paper
• Demo: The Neural Network Verification (NNV) Tool

  2020cites this paper
• EXTENDING FLOWPIPE CONSTRUCTION FOR COMPOSITIONAL HYBRID AUTOMATA

  2020cites this paper
• ARCH-COMP20 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

  2020cites this paper
• ForFET SMT : Quantitative SMT Analysis of Hybrid Automata using Features ∗

  2020cites this paper
• Demo Abstract: A CPS Toolchain for Learning-based Systems

  2019cites this paper
• Aggregation Strategies in Reachable Set Computation of Hybrid Systems

  2019cites this paper
• Verification of Continuous and Hybrid Systems ARCH-COMP 19 Repeatability Evaluation Report

  2019cites this paper
• Reachability Analysis for High-Index Linear Differential Algebraic Equations

  2019cites this paper
• Verification of Closed-loop Systems with Neural Network Controllers

  2019cites this paper
• REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency

  2019cites this paper
• A CPS toolchain for learning-based systems: demo abstract

  2019cites this paper
• Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects

  2019cites this paper
• ARCH-COMP19 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants

  2019cites this paper
• Simulation-based verification of bounded-horizon safety for hybrid systems using dynamic number of simulations

  2019cites this paper
• Reachability Analysis of Power Electronic Converters

  2019influential citation
• Design and validation of Cyber-Physical Systems through model abstraction*

  2019cites this paper
• Demo: a design studio for verification tools

  2019cites this paper
• Reachability Analysis of Dual Active Bridge DC-DC Converters

  2019influential citation
• Applied Verification of Continuous and Hybrid Systems ARCH-COMP 18 Repeatability Evaluation Report

  2018cites this paper
• The present work was submitted to the LuFG Theory of Hybrid Systems M ASTER OF S CIENCE T HESIS C OMPARING THE EXPRESSIVITY AND USABILITY OF HYBRID SYSTEMS ’ MODELING LANGUAGES

  2018cites this paper
• Parallel reachability analysis of hybrid systems in XSpeed

  2018cites this paper
• Reachability Analysis and Safety Verification for Neural Network Control Systems

  2018cites this paper
• Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process. (Vérification formelle des systèmes cyber-physiques dans le processus industriel de la conception basée sur modèle)

  2018cites this paper
• Automatically Finding Bugs in a Commercial Cyber-Physical System Development Tool Chain With SLforge

  2018cites this paper
• Algorithmic Attack Synthesis Using Hybrid Dynamics of Power Grid Critical Infrastructures

  2018cites this paper
• CYBER-PHYSICAL SYSTEMS: FROM SPECIFICATION INFERENCE TO DESIGN ANALYSIS

  2018influential citation
• A Framework for Inference and Identification of Hybrid-System Models: Mixed Event-/Time-driven Systems (METS)

  2018cites this paper
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

  2018influential citation
• High-level Hybrid Systems Analysis with Hypy

  2017cites this paper
• Satisfiability Modulo Transcendental Functions via Incremental Linearization

  2017cites this paper
• Time-Triggered Conversion of Guards for Reachability Analysis of Hybrid Automata

  2017cites this paper
• Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

  2017cites this paper
• formalSpec - Semi-Automatic Formalization of System Requirements for Formal Verification

  2017cites this paper
• Rigorous Simulation-Based Analysis of Linear Hybrid Systems

  2017cites this paper
• Reachability Analysis of Transformer-Isolated DC-DC Converters

  2017cites this paper
• Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees

  2017cites this paper
• Compile-Time Extensions to Hybrid ODEs

  2017cites this paper
• HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems

  2017cites this paper
• Modeling the Wind Turbine Benchmark with PWA Hybrid Automata

  2017cites this paper
• Hybrid automata: from verification to implementation

  2017cites this paper
• Direct Verification of Linear Systems with over 10000 Dimensions

  2017cites this paper
• International Workshop on Applied Verification for Continuous and Hybrid Systems Large-Scale Linear Systems from Order-Reduction ( Benchmark Proposal )

  2017cites this paper
• Model Validation of PWM DC–DC Converters

  2017cites this paper
• Constructing verification models of nonlinear Simulink systems via syntactic hybridization

  2017cites this paper
• ARCH-COMP17 Repeatability Evaluation Report

  2017cites this paper
• Charge Pump Phase-Locked Loops and Full Wave Rectifiers for Reachability Analysis

  2017cites this paper
• Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata

  2017cites this paper
• Formal Requirements-Driven Analysis of Cyber Physical Systems

  2017cites this paper
• EPiC Series in Computing

  2017cites this paper
• Formal Verification of Nonlinear Simulink Models via Syntactic Hybridization

  2017cites this paper
• Computer-Aided Formal Verification of Power Electronics Circuits

  2017cites this paper
• Distributed Autonomous Systems (Benchmark Proposal)

  2017cites this paper
• Benchmarks for Non-linear Continuous System Safety Verification

  2016cites this paper
• Direct methods for deductive verification of temporal properties in continuous dynamical systems

  2016cites this paper
• Demo : Hybrid Systems Model Transformations with HyST

  2016cites this paper
• Non-linear Continuous Systems for Safety Verification

  2016cites this paper
• A Compositional Approach to the Verification of Hybrid Systems

  2016cites this paper
• Decomposed Reachability Analysis for Nonlinear Systems

  2016cites this paper
• Decoupling Abstractions of Non-linear Ordinary Differential Equations

  2016cites this paper
• Scalable Static Hybridization Methods for Analysis of Nonlinear Systems

  2016influential citation
• Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP

  2016cites this paper
• SL2SX Translator: From Simulink to SpaceEx Models

  2016cites this paper
• Verifying cyber-physical systems by combining software model checking with hybrid systems reachability

  2016cites this paper
• Order-reduction abstractions for safety verification of high-dimensional linear systems

  2016cites this paper
• Parallel reachability analysis for hybrid systems

  2016cites this paper
• C2E2: a tool for verifying annotated hybrid systems

  2015cites this paper
• Co-Simulation of Hybrid Systems with SpaceEx and Uppaal

  2015influential citation
• Aalborg Universitet Co-Simulation of Hybrid Systems with SpaceEx and

  2015influential citation
• Runtime Verification for Hybrid Analysis Tools

  2015cites this paper
• Benchmark: Stratied Controllers of Tank Networks

  2015cites this paper
• Benchmark: A Nonlinear Reachability Analysis Test Set from Numerical Analysis

  2015cites this paper
• Benchmark : Stratified Controllers of Tank Networks

  2015cites this paper
• Quantified Bounded Model Checking for Rectangular Hybrid Automata

  2015cites this paper
• Continuous and Hybrid Systems Benchmark : Stratified Controllers of Tank Networks ∗

  2015cites this paper
• Periodically-Scheduled Controller Analysis Using Hybrid Systems Reachability and Continuization

  2015influential citation
• Current Challenges in the Verification of Hybrid Systems

  2015cites this paper
• Real-Time Reachability for Verified Simplex Design

  2014cites this paper