ANALYSIS OF APPROACHES TO THE SIMULATION AND VERIFICATION OF CYBER-PHYSICAL SYSTEMS

Authors

  • S. U. Korotunov National University “Zaporizhia Polytechnic”, Zaporizhzhia, Ukraine
  • G. V. Tabunshchyk National University “Zaporizhia Polytechnic”, Zaporizhzhia, Ukraine

DOI:

https://doi.org/10.15588/1607-3274-2020-3-5

Keywords:

Verification, cyber-physical system, Kripke structure, finite state machine, temporal logic, model verification, simulation.

Abstract

Context. Current trends in the performance and complexity of system requirements require fundamentally new approaches to design, in which cybernetic and physical components are integrated at different stages. Cyber-physical systems are systems that provide close interaction between physical and cybernetic components, integration of computing, physical processes and networks. In such systems, software and physical subsystems operate in different temporal and spatial dimensions, interacting in different ways. Cyberphysical systems surround humans in almost every area of existence, from housing and transportation to medical devices and interregional power grids. Therefore, verification and validation of such systems is an urgent task today. Approaches to verification of cyber-physical systems are considered. The object of research is the process of verification of cyber-physical systems, the subject is the methods of verification of cyber-physical systems, models and logic used in formal verification.

Objective. The purpose of the work is to analyze approaches to the verification of cyber-physical systems, detailing the individual steps, such as the selection of models, verification tools, and, in fact, verification methods.

Method. The main methods outlined in the paper are methods of formal verification of cyber-physical systems, namely simulation, theorem proving, symbolic execution, and model checking. In addition, the methodology of the model checking method – the Kripke structure and temporal logics: logic of computational trees and linear time logic is discussed in detail. Modeling using finite state machines is also performed. 

Results. The paper deals with modeling of the cyber-physical system in the form of creation of the Kripke structure that allowed to describe all states of the system necessary for executing of formal verification.

Conclusions. The paper describes the characteristics of cyber-physical systems, analyzes the methods of verification of such systems. After analysis the conclusion is made about the most promising method of model verification, for which the basic methodology is considered. Characteristics of Kripke structure and temporal logics are described as the main elements of the model checking method. Following the review, the shortcomings of the standard methodology most relevant to the modeling stage of cyber-physical systems are concluded. The possibility of using finite state machines, namely Kripke structures, for modeling elements of a cyber-physical system is shown. The scientific novelty of the work is that models of cyber-physical systems have been developed, which, unlike existing ones, are based on Kripke structures, which allow to make a detailed description of all states of the system, which, in turn, is an important step to verify such a system. The practical value of the work is the developed models of the independent power station of alternative energy, which will automate the process of charging electric vehicles. Digital duplicates have been implemented, which allow modeling the processes of an independent energy station of alternative energy. The developed duplicates are used in the study of disciplines in the preparation of bachelors and masters in 121 computer science.

Author Biographies

S. U. Korotunov, National University “Zaporizhia Polytechnic”, Zaporizhzhia

Postgraduate student at the Department of Software

G. V. Tabunshchyk, National University “Zaporizhia Polytechnic”, Zaporizhzhia

PhD, Professor of the Department of Software

References

Workshop on cyber-physical systems [Electronic resource] – Access mode: http://varma.ece.cmu.edu/CPS

Johnson T. T., Mitra S. Parametrized verification of distributed cyber-physical systems: an aircraft landing protocol case study, Cyber-Physical Systems, Third international conference, Beijing, 17–19 April 2012, proceedings. Beijing, IEEE/ACM, 2012, P. 161–170. DOI: 10.1109/iccps.2012.24

Pajic M., Jiang Z., Lee I. et al. From verification to implementation: a model translation tool and a pacemaker case study, IEEE 18th Real Time and Embedded Technology and Applications Symposium. Beijing, 2012, pp. 173–184. DOI: 10.1109/rtas.2012.25

Mo Y., Kim T. H., Brancik K. et al. Cyber-physical security of a smart grid infrastructure, Proceedings of the IEEE, 2012, Vol. 100, № 1, pp. 195–209. DOI: 10.1109/jproc.2011.2161428

Rajkumar R., Lee I., Sha L. et al. Cyber-physical systems: the next computing revolution, Design Automation, 47th international conference, Anaheim, 13–18 June 2010, proceedings. Anaheim, IEEE, 2010, pp. 731–736. DOI: 10.1145/1837274.1837461

Cyber-Physical Systems [Electronic resource]. Access mode: https://www.nsf.gov/pubs/2010/nsf10515/nsf10515.htm

Miclea L., Sanislav T. About dependability in cyberphysical systems, 9th East-West Design & Test Symposium (EWDTS). Sevastopol, 2011, pp. 17–21. DOI: 10.1109/EWDTS.2011.6116428

McConnell S. Code complete. Redmond, Microsoft Press, 2009, 960 p.

Lloyd S. Programming the Universe: A Quantum Computer Scientist Takes on the Cosmos. New York, Knopf, 2006, 240 p.

Korotunov S., Tabunshchyk G., Wolff C. Cyber-physical systems architectures and modeling methods analysis for smart grids, Computer Sciences and Information Technologies , 13th International Scientific and Technical Conference. Lviv, 11–14 Sept. 2018, proceedings. Lviv, IEEE, 2018, pp. 181–186. DOI: 10.1109/STCCSIT.2018.8526726

Gupta S., Mukherjee T., Venkatasubramanian K. Safety Body area networks: safety, security, and sustainability. Cambridge, Cambridge University Press, 2013, Section 4, 36 p. DOI: 10.1017/CBO9781139108126.006

Kernbach S., Kornienko O., Levi P. Generation of desired emergent behavior in swarm of micro-robots, Artificial Intelligence, 16th Eureopean Conference, Valencia, 22–27 August 2004, proceedings. Valencia, IOS Press, 2004, Vol. 110, P. 239–243.

Song H., Rawat D. B., Jeschke S. et al. Cyber-Physical Systems. Foundations, Principles and Applications. Cambridge, Academic Press, 2017, 514 p.

Korotunov S., Tabunshchyk G., Henke K. et al. Analysis of the verification approaches for the cyberphysical systems, Third International Workshop on Computer Modeling and Intelligent Systems (CMIS). Zaporizhzhia, 2019, pp. 950– 961.

Habra N., Abran A., Lopez M. et al. A framework for the design and verification of software measurement methods, Journal of Systems and Software, 2008, Vol. 81, № 5, pp. 633–648. DOI: 10.1016/j.jss.2007.07.038.

Subbotin S. A. Diagnostic models synthesis method based on radial basis neural networks with support for shorthand properties, Radío Electronics, Computer Science, Control, 2016, № 2 (37), pp. 64–69. DOI: 10.15588/1607-32742016-2-8

Tuch H. OS Verification – Now! [Electronic resource]. Access mode: https://www.usenix.org/legacy/event/hotos05/final_papers_b ackup/tuch/tuch_html/index.html

Cervin A., Henriksson D., Lincoln B. How does control timing affect performance? Analysis and simulation of timing using Jitterbug and TrueTime, IEEE Control Systems Magazine, 2003, Vol. 23, № 3, pp. 16–30. DOI: 10.1109/MCS.2003.1200240

Li B., Sun Z., Mechitov K. et al. Realistic case studies of wireless structural control, Cyber-Physical Systems, 4th international conference, Philadelphia, 8–11 April 2013, proceedings. Philadelphia, IEEE, 2013, pp. 179–188. DOI: 10.1109/ICCPS.2013.6604012

Kohtamaki T., Pohjola M., Brand J. et al. PiccSIM Toolchain – design, simulation and automatic implementation of wireless networked control systems, Networking, Sensing and Contro, International conference, Okayama, 26–29 March 2009, proceedings. Okayama, IEEE, 2009, pp. 49–54. DOI:10.1109/ICNSC.2009.4919244

Eyisi E., Bai J., Riley D. et al. NCSWT: An integrated modeling and simulation tool for networked control systems, Simulation Modelling Practice and Theory, 2012, Vol. 27, pp. 90–111. DOI: 10.1016/j.simpat.2012.05.004

Kiddle C., Simmonds R., Williamson C. et al. Hybrid packet/fluid flow network simulation, Seventeenth Workshop on Parallel and Distributed Simulation (PADS). San Diego, 2003, pp. 143–152. DOI: 10.1109/PADS.2003.1207430

Liu J. Parallel simulation of hybrid network traffic models, 21st International Workshop on Principles of Advanced and Distributed Simulation, 2007, pp. 141–151. DOI: 10.1109/PADS.2007.26

Melamed B., Pan S., Wardi Y. HNS: A streamlined hybrid network simulator, ACM Transactions on Modeling and Computer Simulation, 2004, Vol. 14, № 3, pp. 251–277. DOI: 10.1145/1010621.1010623

Platzer A., Quesel J. D. KeYmaera: a hybrid theorem prover for hybrid systems (system description), Automated Reasoning, 4th International Joint Conference, Berlin Heidelberg, 12–15 August 2008, proceedings. Berlin, Springer-Verlag, 2008, pp. 171–178. DOI: 10.1007/978-3540-71070-7_15

Banerjee A., Gupta K. S. Spatio-temporal hybrid automata for safe cyber-physical systems: A medical case study, Cyber-Physical Systems, 4th international conference, Philadelphia, 8–11 April 2013, proceedings. Philadelphia, ACM/IEEE, 2013, pp. 71–80. DOI: 10.1145/2502524.2502535

Formal software verification: model checking and theorem proving : Embedded Systems Laboratory Technical Report : ESL-TIK-00214 / Massachusetts Institute of Technology ; M. Ouimet. Cambridge, 2007, 12 p.

Bagade P., Banerjee A., Gupta S. K. Safety assurance of medical cyber-physical systems using hybrid automata: a case study on analgesic infusion pump, Medical CPS Workshop, 2013, pp. 111–118. DOI: 10.1.1.294.6604

Sasnauskas R., Dustmann O. S., Kaminski B. L. et al. Scalable symbolic execution of distributed systems, Distributed Computing Systems, 31st International Conference, Minneapolis, 20–24 June 2011, proceedings. Minneapolis, IEEE, 2011, pp. 333–342. DOI: 10.1109/ICDCS.2011.28

Majumdar R., Saha I., Shashidhar K. C. et al. CLSE: closedloop symbolic execution, NASA Formal Methods Symposium, 2012, pp. 356–370. DOI: 10.1007/978-3-64228891-3_33

Pasareanu C. S., Rungta N. Symbolic PathFinder: symbolic execution of Java bytecode, Automated Software Engineering, 25th international conference, Antwerp, 20–24 September 2010, proceedings. Antwerp, IEEE/ACM, 2010, pp. 179–180. DOI: 10.1145/1858996.1859035

Clarke E. M., Zuliani P. Statistical model checking for cyber-physical systems, Automated Technology for Verification and Analysis, 9th International Symposium, Taipei, 2011, Vol. 6996, pp. 1–12. DOI: 10.1007/978-3-64224372-1_1

Kalajdzic K., Jegourel C., Lukina A. et al. Feedback control for statistical model checking of cyber-physical systems, International Symposium on Leveraging Applications of Formal Methods, 2016, Vol. 9952, pp. 46–61. DOI: 10.1007/978-3-319-47166-2_4

Clarke E. M., Emerson E. A., Sistla A. P. Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1983, pp. 117–126. DOI: 10.1145/567067.567080

Dijkstra E. W. The humble programmer, Communications of the ACM, 1972, Vol. 15, № 10, pp. 859–866. DOI: 10.1145/355604.361591

Subbotin S. A. Synthesis of neuro-fuzzy networks ranking and specific encoding attributes for diagnostics and automatic classification of the precedents, Radío Electronics, Computer Science, Control, 2016, № 1 (36), pp. 50–57. DOI: 10.15588/1607-3274-2016-1-6

Abraham-Mumm E., Hannemann U., Steffen M. Verification of hybrid systems: formalization and proof rules in PVS, Engineering of Complex Computer Systems, 7th international conference, Skovde, 11–13 June 2001, proceedings. Skovde, IEEE, 2001, pp. 48–57. DOI:10.1109/ICECCS.2001.930163

Clarke E. M., Henzinger T. A., Veith H. et al. Handbook of Model Checking. Cham, Springer International Publishing, 2018, 1210 p.

Clarke E. M. Model Checking / E. M. Clarke, O. Grumberg, В. Peled. Cambridge : MIT Press, 2001, 314 p.

Gabbay D. Semantical Considerations for Modal Logics by Saul A. Kripke, The Journal of Symbolic Logic, 1969, Vol. 34, № 3, P. 501. DOI: 10.2307/2270922

Pnueli A. The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (SFCS), Providence, 1977, pp. 46–57. DOI: 10.1109/SFCS.1977.32

Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic, Workshop on Logic of Programs, 1982, pp. 52–71.

Arras P., Tabunshchyk G., Okhmak V. et al. Modeling and simulation of the services for vehicle charging infrastructure interaction, Intelligent Data Acquisition and Advanced Computing Systems, Technology and Applications, 10th international conference, Metz, 18–21 September 2019: proceedings. Metz, IEEE, 2019, pp. 330–333. DOI: 10.1109/IDAACS.2019.8924449

Tabunshchyk G., Arras P., Korotunov S. et al. Cost optimization simulation for electric vehicle charging infrastructure, IEEE European Technology & Engineering Management Summit (ETEMS). Dortmund, 2020, pp. 76–88.

McNaughton R. Elementary computability, formal languages, and automata. Lawrence : Z B Publishing Industries, 1993, 400 p.

Arras P., Tabunshchyk G. Type or paste your text here to design optimization techniques in mechanical design and education of engineers convert case, Advances in Design, Simulation and Manufacturing, 2020, pp. 13–22. DOI: 10.1007/978-3-030-22365-6_2

Korotunov S., Tabunshchyk G., Okhmak V. Genetic algorithms as an optimization approach for managing electric vehicles charging in the Smart Grid, Computer Modeling and Intelligent Systems, 3rd international workshop, Zaporizhzhia, 27–01 May 2020, proceedings. Zaporizhzhia, CEUR WS, 2020, pp. 184–198.

How to Cite

Korotunov, S. U., & Tabunshchyk, G. V. (2020). ANALYSIS OF APPROACHES TO THE SIMULATION AND VERIFICATION OF CYBER-PHYSICAL SYSTEMS. Radio Electronics, Computer Science, Control, (3), 57–68. https://doi.org/10.15588/1607-3274-2020-3-5

Issue

Section

Mathematical and computer modelling