Abstract
Model-based design (MBD) in systems engineering is a well-accepted technique to abstract, analyze, verify, and validate complex systems. In MBD, we design a mathematical model of the system to virtually execute and test systems via model simulations to understand the system dynamics better. Computing model simulations have their challenges: one is to ensure that the simulation trajectory preserves the model semantics. Besides, computing many simulation trajectories over a long time-horizon must be time-efficient for rapid response to system engineers. In this work, we address these challenges in simulating models of Cyber-Physical-Systems (CPS), particularly systems possessing mixed discrete-continuous dynamics. We focus on the subclass of CPS’s hybrid-automata models, where jump predicates are restricted to polygonal constraints and present a numerical simulation engine that can efficiently compute many random simulations in parallel by exploiting the parallel computing capability in modern multicore processors. Our simulation engine implements a lock-free parallel breadth-first-search (BFS) like algorithm and is implemented in the model-checking tool XSpeed. We demonstrate the performance gains of our simulation engine over SpaceEx and CORA, the modern model checkers and simulators for affine hybrid systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Althoff M (2010) Reachability analysis and its application to the safety assessment of autonomous cars. PhD thesis, Technische Universität München
Althoff M, Grebenyuk D (2016) Implementation of interval arithmetic in cora 2016. In: ARCH@ CPSWeek, pp 91–105
Alur, R.: Principles of cyber-physical systems. MIT Press (2015)
Alur R, Courcoubetis C, Henzinger TA, Ho PH (1992) Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Hybrid systems. Springer, pp 209–229
Alur R, Dill DL (1994) A theory of timed automata. Theoretical computer science 126(2):183–235
Antoulas AC, Sorensen DC, Gugercin S (2001) A survey of model reduction methods for large-scale systems. Contemporary Mathematics 280:193–219
Bak S, Duggirala PS (2017) Hylaa: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th international conference on hybrid systems: computation and control. ACM, pp. 173–178
Brand D, Zafiropulo P (1983) On communicating finite-state machines. Journal of the ACM (JACM) 30(2):323–342
Coddington EA, Levinson N (1955) Theory of ordinary differential equations. Tata McGraw-Hill Education
Damm W, Harel D (2001) Lscs: Breathing life into message sequence charts. Formal methods in system design 19(1):45–80
Donze A (2010) Breach: a toolbox for verification and parameter synthesis of hybrid systems. In: In Computer-aided verification, pp 167–170
Duggirala PS, Mitra S, Viswanathan M, Potok M (2015) C2e2: a verification tool for stateflow models. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 68–82
Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. In: HSCC, vol 4. Springer, pp 326–341
Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R. Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV. LNCS, vol 6806. Springer, pp 379–395
Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R (2016) Parallel reachability analysis for hybrid systems. In: 2016 ACM/IEEE international conference on formal methods and models for system design (MEMOCODE). IEEE, pp 12–22
Gurung A, Ray R, Bartocci E, Bogomolov S, Grosu R (2018) Parallel reachability analysis of hybrid systems in XSpeed. Int J Softw Tools Technol Transf 1–23
Hainry E (2008) Reachability in linear dynamical systems. In: Conference on computability in Europe. Springer, pp 241–250
Henzinger TA (2000) The theory of hybrid automata. In: Verification of digital and hybrid systems. Springer, pp 265–292
Holzmann GJ (2012) Parallelizing the SPIN model checker. In: Proceedings of SPIN 2012. LNCS, vol 7385. Springer, pp 155–171
Jensen JC, Chang DH, Lee EA (2011) A model-based design methodology for cyber-physical systems. In: 2011 7th international wireless communications and mobile computing conference. IEEE, pp 1666–1671
Jin X, Deshmukh JV, Kapinski J, Ueda K, Butts K (2014) Powertrain control verification benchmark. In: Proceedings of the 17th international conference on Hybrid systems: computation and control. ACM, pp. 253–262
Lee EA, Seshia SA (2016) Introduction to embedded systems: a cyber-physical systems approach. MIT Press
Lygeros J, Tomlin C, Sastry S (1999) Hybrid systems: modeling, analysis and control. preprint
Makhlouf IB, Kowalewski S (2014) Networked cooperative platoon of vehicles for testing methods and verification tools. In: ARCH@ CPSWeek, pp 37–42
Mathworks: Model-Based Design (2020). https://www.mathworks.com/solutions/model-based-design.html
Paterno F (1999) Model-based design and evaluation of interactive applications. Springer Science & Business Media
Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R (2015) Xspeed: accelerating reachability analysis on multi-core processors. In: Piterman N (ed) Hardware and software: verification and testing—11th international haifa verification conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9434. Springer, pp 3–18. https://doi.org/10.1007/978-3-319-26287-1_1
Reisig W (2012) Petri nets: an introduction, vol 4. Springer Science & Business Media
Serban R, Hindmarsh AC (2005) Cvodes: the sensitivity-enabled ode solver in sundials. In: ASME 2005 international design engineering technical conferences and computers and information in engineering conference. American Society of Mechanical Engineers, pp 257–269
Skogestad S, Postlethwaite I (2005) Multivariable Feedback Control: Analysis and Design. John Wiley & Sons
Acknowledgements
Rajarshi Ray gratefully acknowledges financial support from the Science and Engineering Research Board (SERB) project with file number IMP/2018/000523. Amit Gurung is grateful to Martin Luther Christian University, Shillong, Meghalaya, for partially supporting the work under project grant No. Seed-Grant/559/2017-5567.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this chapter
Cite this chapter
Das, K., Gurung, A., Ray, R. (2021). Parallel Simulation of Cyber-Physical-Systems. In: Chaki, R., Chaki, N., Cortesi, A., Saeed, K. (eds) Advanced Computing and Systems for Security: Volume 14. Lecture Notes in Networks and Systems, vol 242. Springer, Singapore. https://doi.org/10.1007/978-981-16-4294-4_1
Download citation
DOI: https://doi.org/10.1007/978-981-16-4294-4_1
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-16-4293-7
Online ISBN: 978-981-16-4294-4
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)