We have developed a number of algorithms to efficiently analyze hybrid systems. In particular, we have worked on the following projects:
- SpaceEx bug finder. We have developed a version of SpaceEx adjusted towards solving falsification problems, i.e., our primary goal is to find a path to the bad states as fast as possible. To this end, we have introduced two heuristics which prioritize symbolic successors during the exploration of the state space of a considered hybrid system: box-based heuristicand PDB heuristic.
- Composition reasoning in SpaceEx. We have investigated the application of compositional methods to hybrid systems. We have implemented a version of SpaceEx incorporating assume-guarantee abstraction refinement schema (AGAR).
- Benchmark suite. We provide a parameterized benchmark generator for stratified controllers of tank networks.
- SpaceEx-Simulink translation. We have developed a source-to-source translation from SpaceEx models to Simulink.
- Support-function based refinement framework for hybrid systems. We have developed a version of SpaceEx which automatically refines the region representation based on transition guards and bad states. In this way, we can leverage precision and performance.
- Functional Mock-Up Interface support in SpaceEx. We have integrated FMI into SpaceEx and Uppaal to support co-simulation of hybrid and timed systems.
- Parameter identification for hybrid systems. We have proposed an abstraction based framework to identify parameters of multi-affine dynamic systems for a given safety property.