A comparative analysis of existing approaches to Cyber-Physical Systems simulation has been conducted. The intrinsic peculiarities of Cyber-Physical Systems have been reasoned and generalized. Thelimitations of available simulation tools have been pointed out. The approach to Cyber-Physical Systems design solutions checking on the basis of timed automata, UPPAAL integrated tool environment and Temporal Logic of Actions usage has been proposed. The proposed approach is supposed to be applied at designing stage — to prevent the potential time and computational expenses on overcomplicated or faulty formal models checking. A case study on electric power delivery system usage scenario has been conducted.
[1] J. Lee, B. Bagheri, and H.-A. Kao, «A Cyber-Physical Systems architecture for Industry 4.0-based manufacturing systems», Manufacturing Letters, vol. 3, pp. 18-23, Jan. 2015.
https://doi.org/10.1016/j.mfglet.2014.12.001
[2] E. A. Lee, «Cyber Physical Systems: Design Challenges», in Proc. 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), Orlando, FL, USA, 2008, pp. 363-369.
https://doi.org/10.1109/ISORC.2008.25
[3] E.M. Clarke and P. Zuliani, «Statistical Model Checking for Cyber-Physical Systems», ATVA 2011, Lecture Notes in Computer Science, vol. 6996, pp. 1-12, 2011.
https://doi.org/10.1007/978-3-642-24372-1_1
[4] P. Derler, E. A. Lee, and A. S. Vincentelli, «Modeling cyber-physical systems», Proceedings of the IEEE, vol. 100, no. 1, pp. 13-28, Jan. 2012.
https://doi.org/10.1109/JPROC.2011.2160929
[5] D. Henriksson and H. Elmqvist, «Cyber-Physical Systems Modeling and Simulation with Modelica», in Proc. 8th Modelica Conference, Dresden, Germany, 2011, pp. 502-509.
https://doi.org/10.3384/ecp11063502
[6] S. Weyer, T. Meyer, M. Ohmer, D. Gorecky, and D. Zühlke, «Future Modeling and Simulation of CPS-based Factories: an Example from the Automotive Industry», IFAC-PapersOnLine, vol. 49, no. 31, pp. 97-102, 2016.
https://doi.org/10.1016/j.ifacol.2016.12.168
[7] K. H. Lee, J. H. Hong, and T. G. Kim, «System of Systems Approach to Formal Modeling of CPS for Simulation-Based Analysis», ETRI Journal, vol. 37, no. 1, pp. 175-185, Feb. 2015.
https://doi.org/10.4218/etrij.15.0114.0863
[8] J. C. Jensen, D. H. Chang, and E. A. Lee, «A model-based design methodology for cyber-physical systems», in Proc. 2011 7th International Wireless Communications and Mobile Compu-ting Conference, Istanbul, Turkey, Jul. 2011, pp. 1666-1671.
https://doi.org/10.1109/IWCMC.2011.5982785
[9] J. E. Kim and D. Mosse, «Generic framework for design, modeling and simulation of cyber physical systems», ACM SIGBED Review, vol. 5, no. 1, pp. 1-2, Jan. 2008.
https://doi.org/10.1145/1366283.1366284
[10] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. Massachusetts: MIT Press, 2001, 309 p.
[11] J. Shi, J. Wan, H. Yan, and H. Suo, «A survey of cyber-physical systems», in Proc. 2011 International Conference on Wireless Communications and Signal Processing (WCSP), Nanjing, China, Nov. 2011, pp. 1-6.
https://doi.org/10.1109/WCSP.2011.6096958
[12] E.A. Lee, «The Past, Present and Future of Cyber-Physical Systems: A Focus on Models», Sensors, vol. 15, no. 3, pp. 4837-4869, 2015.
https://doi.org/10.3390/s150304837
[13] C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker, and M. Deardeuff, «How Amazon web services uses formal methods», Communications of the ACM, vol. 58, no. 4, pp. 66-73, 2015.
https://doi.org/10.1145/2699417
[14] L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc., 2002, 348 p.
[15] Y-M. Kim, M. Kang, and J-Y. Choi, «Formal Specification and Verification of Firewall using TLA+», in Proc. 2017 International Conference on Security and Management, SAM'17, Las Vegas, Nevada, USA, Jul. 2017, pp. 247-251.
[16] S. Resch and M. Paulitsch, «Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware», in Proc. 2017 IEEE International Symposium on Software Reliability Engineering Workshops, ISSREW 2017, Toulouse, France, Oct. 2017, pp. 146-152.
https://doi.org/10.1109/ISSREW.2017.43
[17] V. V. Shkarupylo, I. Tomicic, K. M. Kasian, and J. A. J. Al-sayaydeh, «An Approach to increase the Effectiveness of TLC Verification with Respect to the Concurrent Structure of TLA+ Specification», International Journal of Software Engineering and Computer Systems, vol. 4, no. 1, pp. 48-60, 2018.
https://doi.org/10.15282/ijsecs.4.1.2018.4.0037
[18] V. V. Shkarupylo, I. Tomicic, and K. M. Kasian, «The investigation of TLC model checker properties», Journal of Information and Organizational Sciences, vol. 40, no. 1, pp. 145-152, 2016.
https://doi.org/10.31341/jios.40.1.7
[19] G. Behrmann, A. David, and K.G. Larsen, «A Tutorial on Uppaal», Formal Methods for the Design of Real-Time Systems. SFM-RT 2004. Lecture Notes in Computer Science, vol. 3185, pp. 200-236, 2004.
https://doi.org/10.1007/978-3-540-30080-9_7
[20] J.H. Kim, K.G. Larsen, B. Nielsen, M. Mikucionis, and P. Olsen, «Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools», Formal Methods for Industrial Critical Systems. FMICS 2015. Lecture Notes in Computer Science, vol. 9128, pp. 47-61, 2015.
https://doi.org/10.1007/978-3-319-19458-5_4
[21] Y. Liu, Y. Peng, B. Wang, S. Yao, and Z. Liu, «Review on cyber-physical systems», IEEE/CAA Journal of Automatica Sinica, vol. 4, no. 1, pp. 27-40, 2017.
https://doi.org/10.1109/JAS.2017.7510349
[22] V. Shkarupylo and O. Polska, «The Approach to SDN Network Topology Verification on a Basis of Temporal Logic of Actions», in Proc. 14th Int. Conf. on Advanced Trends in Radio-electronics, Telecommunications and Computer Engineering, TCSET'2018, Lviv-Slavske, Ukraine, Feb. 2018, pp. 183-186.
https://doi.org/10.1109/TCSET.2018.8336182