Top

Published in:

2019 | OriginalPaper | Chapter

Reliable Simulation and Monitoring of Hybrid Systems Based on Interval Analysis

(Extended Abstract)

Authors : Daisuke Ishii, Alexandre Goldsztejn, Naoki Yonezaki

Published in: Cyber Physical Systems. Design, Modeling, and Evaluation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Template-Based Monte-Carlo Test Generation for Simulink Models

next chapter An Integrated Simulation Tool for Computer Architecture and Cyber-Physical Systems

https://www.mathworks.com/products/matlab.html.

https://www.modelica.org/.

Alur, R., et al.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995)MathSciNetCrossRef

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)

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)

Collins, P., Goldsztejn, A.: The reach-and-evolve algorithm for reachability analysis of nonlinear dynamical systems. Electron. Notes Theor. Comput. Sci. 223(639), 87–102 (2008)CrossRef

Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_9CrossRefMATH

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)

Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_14CrossRef

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30CrossRef

Goldsztejn, A., Ishii, D.: A parallelotope method for hybrid system simulation. Reliable Comput. 23, 163–185 (2016)MathSciNet

10.

Goubault, E., Mullier, O., Kieffer, M.: Inner approximated reachability analysis. In: HSCC, pp. 163–172 (2014)

11.

Ishii, D., Goldsztejn, A.: HySIA: tool for simulating and monitoring hybrid automata based on interval analysis. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 370–379. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_23CrossRef

12.

Ishii, D., Yonezaki, N., Goldsztejn, A.: Monitoring bounded LTL properties using interval analysis. In: 8th International Workshop on Numerical Software Verification (NSV). ENTCS 317, pp. 85–100 (2015)MathSciNetCrossRef

13.

Ishii, D., Yonezaki, N., Goldsztejn, A.: Monitoring temporal properties using interval analysis. In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E99-A (2016)CrossRef

14.

Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15CrossRef

15.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT - 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12CrossRefMATH

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)

17.

Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems. IEEE Trans. Autom. Control 54(10), 2352–2364 (2009)MathSciNetCrossRef

18.

Ramdani, N., Nedialkov, N.S.: Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques. Nonlinear Anal. Hybrid Syst. 5(2), 149–162 (2011)MathSciNetCrossRef

19.

Ratschan, S.: Safety verification of non-linear hybrid systems is quasi-decidable. Formal Methods Syst. Des. 44(1), 71–90 (2014)CrossRef

20.

Sandretto, J.A.D., Chapoutot, A.: Validated explicit and implicit runge-kutta methods. Reliable Comput. 22, 78–103 (2016)MathSciNet

21.

Shmarov, F., Zuliani, P.: ProbReach: Verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC, pp. 134–139 (2015)

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)

Title: Reliable Simulation and Monitoring of Hybrid Systems Based on Interval Analysis
Authors: Daisuke Ishii
Alexandre Goldsztejn
Naoki Yonezaki
Publisher: Springer International Publishing
Book: Cyber Physical Systems. Design, Modeling, and Evaluation
Print ISBN: 978-3-030-17909-0

Electronic ISBN: 978-3-030-17910-6

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-17910-6_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner