On the approaches to cyber-physical systems simulation

dc.citation.epage54
dc.citation.issue1
dc.citation.spage51
dc.contributor.affiliationZaporizhzhia National Technical University
dc.contributor.authorShkarupylo, Vadym
dc.contributor.authorKudermetov, Ravil
dc.contributor.authorPolska, Olga
dc.coverage.placenameЛьвів
dc.date.accessioned2020-02-18T13:14:54Z
dc.date.available2020-02-18T13:14:54Z
dc.date.created2018-02-01
dc.date.issued2018-02-01
dc.description.abstractA 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. The limitations 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.
dc.format.extent51-54
dc.format.pages4
dc.identifier.citationShkarupylo V. On the approaches to cyber-physical systems simulation / Vadym Shkarupylo, Ravil Kudermetov, Olga Polska // Advances in Cyber-Physical Systems. — Lviv : Lviv Politechnic Publishing House, 2018. — Vol 3. — No 1. — P. 51–54.
dc.identifier.citationenShkarupylo V. On the approaches to cyber-physical systems simulation / Vadym Shkarupylo, Ravil Kudermetov, Olga Polska // Advances in Cyber-Physical Systems. — Lviv Politechnic Publishing House, 2018. — Vol 3. — No 1. — P. 51–54.
dc.identifier.urihttps://ena.lpnu.ua/handle/ntb/45682
dc.language.isoen
dc.publisherLviv Politechnic Publishing House
dc.relation.ispartofAdvances in Cyber-Physical Systems, 1 (3), 2018
dc.relation.references1. 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.
dc.relation.references2. 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.
dc.relation.references3. 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.
dc.relation.references4. P. Derler, E. A. Lee, and A. S. Vincentelli, “Modeling cyberphysical systems”, Proceedings of the IEEE, vol. 100, no. 1, pp. 13–28, Jan. 2012.
dc.relation.references5. D. Henriksson and H. Elmqvist, “Cyber-Physical Systems Modeling and Simulation with Modelica”, in Proc. 8th Modelica Conference, Dresden, Germany, 2011, pp. 502–509.
dc.relation.references6. 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.
dc.relation.references7. 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.
dc.relation.references8. J. C. Jensen, D. H. Chang, and E. A. Lee, “A model-based design methodology for cyber-physical systems”, in Proc. 20117th International Wireless Communications and Mobile Computing Conference, Istanbul, Turkey, Jul. 2011, pp. 1666–1671.
dc.relation.references9. 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.
dc.relation.references10. E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. Massachusetts: MIT Press, 2001, 309 p.
dc.relation.references11. 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.
dc.relation.references12. 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.
dc.relation.references13. 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.
dc.relation.references14. 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.
dc.relation.references15. 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.
dc.relation.references16. 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.
dc.relation.references17. V. V. Shkarupylo, I. Tomicic, K. M. Kasian, and J. A. J. Alsayaydeh, “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.
dc.relation.references18. 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.
dc.relation.references19. 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.
dc.relation.references20. 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.
dc.relation.references21. 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.
dc.relation.references22. 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 Radioelectronics, Telecommunications and Computer Engineering, TCSET'2018, Lviv-Slavske, Ukraine, Feb. 2018, pp. 183–186.
dc.relation.referencesen1. 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.
dc.relation.referencesen2. 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.
dc.relation.referencesen3. 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.
dc.relation.referencesen4. P. Derler, E. A. Lee, and A. S. Vincentelli, "Modeling cyberphysical systems", Proceedings of the IEEE, vol. 100, no. 1, pp. 13–28, Jan. 2012.
dc.relation.referencesen5. D. Henriksson and H. Elmqvist, "Cyber-Physical Systems Modeling and Simulation with Modelica", in Proc. 8th Modelica Conference, Dresden, Germany, 2011, pp. 502–509.
dc.relation.referencesen6. 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.
dc.relation.referencesen7. 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.
dc.relation.referencesen8. J. C. Jensen, D. H. Chang, and E. A. Lee, "A model-based design methodology for cyber-physical systems", in Proc. 20117th International Wireless Communications and Mobile Computing Conference, Istanbul, Turkey, Jul. 2011, pp. 1666–1671.
dc.relation.referencesen9. 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.
dc.relation.referencesen10. E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. Massachusetts: MIT Press, 2001, 309 p.
dc.relation.referencesen11. 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.
dc.relation.referencesen12. 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.
dc.relation.referencesen13. 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.
dc.relation.referencesen14. 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.
dc.relation.referencesen15. 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.
dc.relation.referencesen16. 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.
dc.relation.referencesen17. V. V. Shkarupylo, I. Tomicic, K. M. Kasian, and J. A. J. Alsayaydeh, "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.
dc.relation.referencesen18. 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.
dc.relation.referencesen19. 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.
dc.relation.referencesen20. 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.
dc.relation.referencesen21. 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.
dc.relation.referencesen22. 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 Radioelectronics, Telecommunications and Computer Engineering, TCSET'2018, Lviv-Slavske, Ukraine, Feb. 2018, pp. 183–186.
dc.rights.holder© Національний університет “Львівська політехніка”, 2018
dc.rights.holder© Shkarupylo V., Kudermetov R., Polska O., 2018
dc.subjectCyber-Physical System
dc.subjectModel
dc.subjectModel Checking
dc.subjectSimulation
dc.subjectTLA
dc.subjectUPPAAL
dc.subjectVerification
dc.titleOn the approaches to cyber-physical systems simulation
dc.typeArticle

Files

Original bundle

Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
2018v3n1_Shkarupylo_V-On_the_approaches_to_cyber_51-54.pdf
Size:
178.07 KB
Format:
Adobe Portable Document Format
Loading...
Thumbnail Image
Name:
2018v3n1_Shkarupylo_V-On_the_approaches_to_cyber_51-54__COVER.png
Size:
1.52 MB
Format:
Portable Network Graphics

License bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
license.txt
Size:
2.97 KB
Format:
Plain Text
Description: