tuzsutТруды учебных заведений связиProceedings of Telecommunication Universities1813-324X2712-8830СПбГУТ10.31854/1813-324X-2019-5-4-114-123tuzsut-103Research ArticleИНФОРМАТИКА, ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА И УПРАВЛЕНИЕINFORMATICS, COMPUTER ENGINEERING AND MANAGEMENTКомплексная модель защищенных киберфизических систем для их проектирования и верификацииA Comprehensive Model of Secure Cyber-Physical Systems for their Design and VerificationЛевшунД. С.LevshunD. ..levshun@comsec.spb.ruЧечулинА. А.ChechulinA. ..noemail@neicon.ruКотенкоИ. В.KotenkoI. ..noemail@neicon.ruСанкт-Петербургский институт информатики и автоматизации Российской академии наук; Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптикиРоссияSt. Petersburg Institute for Informatics and Automation of the Russian Academy of Science; St. Petersburg National Research University of Information Technologies, Mechanics and OpticsRussian FederationСанкт-Петербургский институт информатики и автоматизации Российской академии наук; Санкт-Петербургский государственный университет телекоммуникаций им. проф. М.А. Бонч-БруевичаРоссияSt. Petersburg Institute for Informatics and Automation of the Russian Academy of Science; The Bonch-Bruevich Saint-Petersburg State University of TelecommunicationsRussian Federation20191304202154114123Copyright © Левшун Д.С., Чечулин А.А., Котенко И.В., 20212021Левшун Д.С., Чечулин А.А., Котенко И.В.Levshun D..., Chechulin A..., Kotenko I...This work is licensed under a Creative Commons Attribution 4.0 License.https://tuzs.sut.ru/jour/article/view/103

В статье предложена комплексная модель защищенных киберфизических систем, предназначенная для их проектирования и верификации. В рамках данной модели киберфизическая система представляется в виде множества блоков с различными свойствами и связями между ними. Основная сложность при построении подобной модели заключается в объединении различных подходов к моделированию киберфизических систем (или их элементов) в рамках единого подхода. Основная цель предлагаемого подхода к моделированию заключается в обеспечении возможности преобразования различных моделей друг в друга без потери значимых данных о блоках системы, а также учете эмерджентных свойств, возникающих в процессе их взаимодействия. Корректность предложенной модели обоснована на примере ее использования для проектирования и верификации системы контроля и управления доступом.

In this paper a combined model of secure cyber-physical systems for their design and verification is proposed. Within the framework of this model, a cyber-physical system is represented as a set of blocks with various properties and relationships between them. The main challenge in such model construction is to combine various approaches to the modeling of cyber-physical systems (or their elements) within a single approach. The main goal of the proposed modeling approach is to provide the ability to convert various models into each other without losing significant data about the elements of the system, as well as taking into account the emergent properties that arise in the process of their interaction. The correctness of the proposed model is validated by the example of its use for design and verification of access control system.

безопасность на основе проектированиякиберфизическая системаверификация безопасностимоделирование системмодель атакующегомодель атакующих действийкомплексная модельsecurity by designcyber-physical systemsecurity verificationsystem modelingattacker modelattack actions modelcomprehensive modelReferencesЛевшун Д.С., Чечулин А.А., Котенко И.В. Проектирование безопасной среды передачи данных на примере протокола I2C // Защита информации. Инсайд. 2018. № 4 (82). С.54-62.Левшун Д.С., Чечулин А.А., Котенко И.В. Проектирование безопасной среды передачи данных на примере протокола I2C // Защита информации. Инсайд. 2018. № 4 (82). С.54-62.Hu F., Lu Y., Vasilakos A.V., Hao Q., Ma R., Patil Y., et al. Robust Cyber-Physical Systems: Concept, Models, and Implementation // Future Generation Computer Systems. 2016. Vol. 56. PP. 449-475. DOI:10.1016/j.future.2015.06.006Hu F., Lu Y., Vasilakos A.V., Hao Q., Ma R., Patil Y., et al. Robust Cyber-Physical Systems: Concept, Models, and Implementation // Future Generation Computer Systems. 2016. Vol. 56. PP. 449-475. DOI:10.1016/j.future.2015.06.006Canedo A., Schwarzenbach E., Faruque M.A.A. Context-sensitive synthesis of executable functional models of cyber-physical systems // Proceeding of the International Conference on Cyber-Physical Systems (ICCPS, Philadelphia, USA, 8-11 April 2013). Piscataway, NJ: IEEE, 2013. PP. 99-108. DOI:10.1145/2502524.2502539Canedo A., Schwarzenbach E., Faruque M.A.A. Context-sensitive synthesis of executable functional models of cyber-physical systems // Proceeding of the International Conference on Cyber-Physical Systems (ICCPS, Philadelphia, USA, 8-11 April 2013). Piscataway, NJ: IEEE, 2013. PP. 99-108. DOI:10.1145/2502524.2502539Srivastava A., Morris T., Ernster T., Vellaithurai C., Pan S., Adhikari U. Modeling Cyber-Physical Vulnerability of the Smart Grid With Incomplete Information // IEEE Transactions on Smart Grid. 2013. Vol. 4. Iss. 1. PP. 235-244. DOI:10.1109/TSG.2012.2232318Srivastava A., Morris T., Ernster T., Vellaithurai C., Pan S., Adhikari U. Modeling Cyber-Physical Vulnerability of the Smart Grid With Incomplete Information // IEEE Transactions on Smart Grid. 2013. Vol. 4. Iss. 1. PP. 235-244. DOI:10.1109/TSG.2012.2232318Xinyu C., Huiqun Y., Xin X. Verification of Hybrid Chi Model for Cyber-Physical Systems Using PHAVer // Proceeding of Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing (Taichung, Taiwan, 3- 5 July 2013). Piscataway, NJ: IEEE, 2013. PP. 122-128. DOI:10.1109/IMIS.2013.29Xinyu C., Huiqun Y., Xin X. Verification of Hybrid Chi Model for Cyber-Physical Systems Using PHAVer // Proceeding of Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing (Taichung, Taiwan, 3- 5 July 2013). Piscataway, NJ: IEEE, 2013. PP. 122-128. DOI:10.1109/IMIS.2013.29Nuzzo P., Sangiovanni-Vincentelli A.L., Bresolin D., Geretti L., Villa T. A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems // Proceedings of the IEEE. 2015. Vol. 103. Iss. 11. PP. 2104-2132. DOI:10.1109/JPROC.2015.2453253Nuzzo P., Sangiovanni-Vincentelli A.L., Bresolin D., Geretti L., Villa T. A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems // Proceedings of the IEEE. 2015. Vol. 103. Iss. 11. PP. 2104-2132. DOI:10.1109/JPROC.2015.2453253Selic B. The pragmatics of model-driven development // IEEE Software. 2003. Vol. 20. Iss. 5. PP. 19-25. DOI:10.1109/MS.2003.1231146Selic B. The pragmatics of model-driven development // IEEE Software. 2003. Vol. 20. Iss. 5. PP. 19-25. DOI:10.1109/MS.2003.1231146Sztipanovits J., Karsai G. Model-integrated computing // Computer. 1997. Vol. 30. Iss. 4. PP. 110-111. DOI:10.1109/2.585163Sztipanovits J., Karsai G. Model-integrated computing // Computer. 1997. Vol. 30. Iss. 4. PP. 110-111. DOI:10.1109/2.585163Kelly S., Tolvanen J.-P. Domain-Specific Modeling: Enabling Full Code Generation. Hoboken: John Wiley & Sons, 2008.Kelly S., Tolvanen J.-P. Domain-Specific Modeling: Enabling Full Code Generation. Hoboken: John Wiley & Sons, 2008.Hehenberger P., Vogel-Heuser B., Bradley D., Eynard B., Tomiyama T., Achiche S. Design, modelling, simulation and integration of cyber physical systems: Methods and applications // Computers in Industry. 2016. Vol. 82. PP. 273-289. DOI:10.1016/j.compind.2016.05.006Hehenberger P., Vogel-Heuser B., Bradley D., Eynard B., Tomiyama T., Achiche S. Design, modelling, simulation and integration of cyber physical systems: Methods and applications // Computers in Industry. 2016. Vol. 82. PP. 273-289. DOI:10.1016/j.compind.2016.05.006Fritzson P. Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Hoboken: John Wiley & Sons, 2010.Fritzson P. Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. Hoboken: John Wiley & Sons, 2010.Penas O., Plateaux R., Patalano S., Hammadi M. Multi-scale approach from mechatronic to Cyber-Physical Systems for the design of manufacturing systems // Computers in Industry. 2017. Vol. 86. PP. 52-69. DOI:10.1016/j.compind.2016.12.001Penas O., Plateaux R., Patalano S., Hammadi M. Multi-scale approach from mechatronic to Cyber-Physical Systems for the design of manufacturing systems // Computers in Industry. 2017. Vol. 86. PP. 52-69. DOI:10.1016/j.compind.2016.12.001Friedenthal S., Alan M. and Rick S. A Practical Guide to SysML: The Systems Modeling Language. Burlington: Morgan Kaufmann, 2014.Friedenthal S., Alan M. and Rick S. A Practical Guide to SysML: The Systems Modeling Language. Burlington: Morgan Kaufmann, 2014.Brück D., Elmqvist H., Olsson H., Mattsson S.E. Dymola for Multi-Engineering Modeling and Simulation. Proceedings of the 2nd International Modelica Conference (Oberphaffenhofen, Germany, 18-19 March 2002). 2002.Brück D., Elmqvist H., Olsson H., Mattsson S.E. Dymola for Multi-Engineering Modeling and Simulation. Proceedings of the 2nd International Modelica Conference (Oberphaffenhofen, Germany, 18-19 March 2002). 2002.Estefan J.A. Survey of Model-Based Systems Engineering (MBSE) Methodologies. URL: http://www.omgsysml.org/MBSE_Methodology_Survey_RevB.pdf (Accessed 21 November 2019)Estefan J.A. Survey of Model-Based Systems Engineering (MBSE) Methodologies. URL: http://www.omgsysml.org/MBSE_Methodology_Survey_RevB.pdf (Accessed 21 November 2019)Rumbaugh J., Blaha M., Premerlani M., Eddy F., Lorensen W. Object-Oriented Modeling and Design. Englewood Cliffs: Prentice-Hall, 1991.Rumbaugh J., Blaha M., Premerlani M., Eddy F., Lorensen W. Object-Oriented Modeling and Design. Englewood Cliffs: Prentice-Hall, 1991.McGuinness D.L., van Harmelen F. OWL Web Ontology Language Overview // W3C recommendation. 2004.McGuinness D.L., van Harmelen F. OWL Web Ontology Language Overview // W3C recommendation. 2004.Balasubramaniyan S., Srinivasan S., Buonopane F., Subathra B., Vain J., Ramaswamy S. Design and verification of Cyber- Physical Systems using TrueTime, evolutionary optimization and UPPAAL // Microprocessors and microsystems. 2016. Vol. 42. PP. 37-48. DOI:10.1016/j.micpro.2015.12.006Balasubramaniyan S., Srinivasan S., Buonopane F., Subathra B., Vain J., Ramaswamy S. Design and verification of Cyber- Physical Systems using TrueTime, evolutionary optimization and UPPAAL // Microprocessors and microsystems. 2016. Vol. 42. PP. 37-48. DOI:10.1016/j.micpro.2015.12.006Ohlin M., Henriksson D., Cervin A. TrueTime 1.5 - Reference Manual. Department of Automatic Control, Lund Institute of Technology, Lund University, 2007.Ohlin M., Henriksson D., Cervin A. TrueTime 1.5 - Reference Manual. Department of Automatic Control, Lund Institute of Technology, Lund University, 2007.Larsen K.G., Pettersson P., Yi W. UPPAAL in a nutshell // International Journal on Software Tools for Technology Transfer (STTT). 1997. Vol. 1. Iss. 1. PP. 134-152.Larsen K.G., Pettersson P., Yi W. UPPAAL in a nutshell // International Journal on Software Tools for Technology Transfer (STTT). 1997. Vol. 1. Iss. 1. PP. 134-152.Seiger R., Keller C., Niebling F., Schlegel T. Modelling complex and flexible processes for smart cyber-physical environments // Journal of Computational Science. 2015. Vol. 10. PP. 137-148. DOI:10.1016/j.jocs.2014.07.001Seiger R., Keller C., Niebling F., Schlegel T. Modelling complex and flexible processes for smart cyber-physical environments // Journal of Computational Science. 2015. Vol. 10. PP. 137-148. DOI:10.1016/j.jocs.2014.07.001Steinberg D., Budinsky F., Merks E., Paternostro M. EMF: Eclipse Modeling Framework. London: Pearson Education, 2008.Steinberg D., Budinsky F., Merks E., Paternostro M. EMF: Eclipse Modeling Framework. London: Pearson Education, 2008.Srinivasan S., Buonopane F., Vain J., Ramaswamy S. Model checking response times in Networked Automation Systems using jitter bounds // Computers in Industry. 2015. Vol. 74. PP. 186-200. DOI:10.1016/j.compind.2015.06.012Srinivasan S., Buonopane F., Vain J., Ramaswamy S. Model checking response times in Networked Automation Systems using jitter bounds // Computers in Industry. 2015. Vol. 74. PP. 186-200. DOI:10.1016/j.compind.2015.06.012Goldblatt R. Logics of Time and Computation. Stanford: Center for the Study of Language and Information, 1992.Goldblatt R. Logics of Time and Computation. Stanford: Center for the Study of Language and Information, 1992.Zainalabedin N. VHDL: Analysis and Modeling of Digital Systems. New York: McGraw-Hill, 1997.Zainalabedin N. VHDL: Analysis and Modeling of Digital Systems. New York: McGraw-Hill, 1997.Fowler M., Scott K. UML Distilled: a Brief Guide to the Standard Object Modeling Language. Boston: Addison-Wesley Professional, 2004.Fowler M., Scott K. UML Distilled: a Brief Guide to the Standard Object Modeling Language. Boston: Addison-Wesley Professional, 2004.Solovyev A., Mikheev M., Zhou L., Dutta-Moscato J., Ziraldo C., An G., et al. SPARK: a framework for multi-scale agentbased biomedical modeling // Proceedings of the Spring Simulation Multiconference (Orlando, USA, 11-15 April 2010). San Diego: Society for Computer Simulation International, 2010. DOI:10.1145/1878537.1878541Solovyev A., Mikheev M., Zhou L., Dutta-Moscato J., Ziraldo C., An G., et al. SPARK: a framework for multi-scale agentbased biomedical modeling // Proceedings of the Spring Simulation Multiconference (Orlando, USA, 11-15 April 2010). San Diego: Society for Computer Simulation International, 2010. DOI:10.1145/1878537.1878541Torti L., Wuillemin P. O3PRM Language Specification. Technical report UPMC. 2013.Torti L., Wuillemin P. O3PRM Language Specification. Technical report UPMC. 2013.Schruben L.W. SIGMA - A graphical approach to teaching simulation // Journal of Computing in Higher Education. 1992. Vol. 4. DOI:10.1007/BF02940978Schruben L.W. SIGMA - A graphical approach to teaching simulation // Journal of Computing in Higher Education. 1992. Vol. 4. DOI:10.1007/BF02940978Десницкий В.А., Чечулин А.А., Котенко И.В., Левшун Д.C., Коломеец М.В. Комбинированная методика проектирования защищенных встроенных устройств на примере системы охраны периметра // Труды СПИИРАН. 2016. № 5(48). C. 5-31. DOI:10.15622/sp.48.1Десницкий В.А., Чечулин А.А., Котенко И.В., Левшун Д.C., Коломеец М.В. Комбинированная методика проектирования защищенных встроенных устройств на примере системы охраны периметра // Труды СПИИРАН. 2016. № 5(48). C. 5-31. DOI:10.15622/sp.48.1Левшун Д.С., Чечулин А.А., Котенко И.В. Жизненный цикл разработки защищенных систем на основе встроенных устройств // Защита информации. Инсайд. 2017. № 4(76). С. 53-59.Левшун Д.С., Чечулин А.А., Котенко И.В. Жизненный цикл разработки защищенных систем на основе встроенных устройств // Защита информации. Инсайд. 2017. № 4(76). С. 53-59.

The authors declare that there are no conflicts of interest present.