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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
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)