Recent advanced languages and tools for hybrid systems

Hybrid systems exhibit both discrete and continuous behavior and thus are notoriously heterogeneous and complex. Over years, there are abundant tools for simulation and verification of hybrid systems. The goal of this paper is to review existing tools as well as presenting recent developed tools for simulation and verification of hybrid systems through classical examples in hybrid academia. Specifically, we use Bouncing Ball, Tank and Thermostat as three examples to illustrate simulation tools of BHPC and Hybrid Chi formalism. In a similar way, classical hybrid system examples (e.g. bouncing ball and tank) are used to illustrate the applicability of the verification tools of KeYmaera, HySAT and iSAT. Afterwards we give a comparative summary for these tools.