Reliable Simulation and Monitoring of Hybrid Systems Based on Interval Analysis
Hybrid systems serve as a high-level model of cyber-physical systems. Formal methods for hybrid systems have been studied energetically for around three decades and various methods for reachability analysis and approximation of continuous states/behaviors have been proposed (e.g., [1, 8]). Another line of technology, e.g., MATLAB/Simulink and Modelica, has been developed in the simulation of hybrid systems and has driven the rise of model-based development in the industry. While reachability analysis methods aim to analyze whole behaviors of a given system with carefully taking care of numerical computation errors, the latter technology focuses on efficient simulation of an approximated trajectory of a practical model.
This work was partially funded by JSPS (KAKENHI 25880008, 15K15968, and 26280024).
- 2.Bouissou, O., Mimram, S., Chapoutot, A.: HySon: set-based simulation of hybrid systems. In: 23rd IEEE International Symposium on Rapid System Prototyping (RSP), pp. 79–85 (2012)Google Scholar
- 3.Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: IEEE Real-Time Systems Symposium, pp. 183–192 (2012)Google Scholar
- 6.Duracz, A., Bartha, F.A., Taha, W.: Accurate rigorous simulation should be possible for good designs. In: Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), pp. 1–10 (2016)Google Scholar
- 10.Goubault, E., Mullier, O., Kieffer, M.: Inner approximated reachability analysis. In: HSCC, pp. 163–172 (2014)Google Scholar
- 16.Mohaqeqi, M., Mousavi, M.R., Taha, W.: Conformance testing of cyber-physical systems: a comparative study. In: 14th International Workshop on Automated Verification of Critical Systems (AVOCS) (2014)Google Scholar
- 21.Shmarov, F., Zuliani, P.: ProbReach: Verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC, pp. 134–139 (2015)Google Scholar
- 22.Wang, Q., Zuliani, P., Kong, S., Gao, S., Clarke, E.M.: SReach: A Bounded Model Checker for Stochastic Hybrid Systems. CoRR abs/1404.7206 (2015)Google Scholar