A type system for formal verification of cyber-physical systems C/C++ software

Yuriy Manzhos, Yevheniia Sokolova

Abstract


The subject: This study focuses on improving the quality of Cyber-Physical System (CPS) software by eliminating incorrect usage of units of measurement and orientation in C/C++ programs. Incorrect usage often leads to critical errors that conventional systems cannot effectively prevent. Manual examination of code using dimensional and orientation analysis can detect these errors in physical equations, but these methods become impractical when dealing with complex physical computations. Objectives: As suggested by Siano, the proposed approach uses physical quantities and prefixes defined by the International System of Units and orientation operations on physical objects. The elaborated system incorporates dimensional and orientation analysis and metaprogramming techniques. The methods used are dimensional & orientational analysis and metaprogramming. The following results were obtained: ensuring consistency of the units, incorporating orientation operations into the programming model for accurately handling physical object rotations and alignments, and using Siano’s work to precisely manipulate object orientation, thereby reducing the likelihood of orientation-related errors. Checking physical dimensions and orientations during the compilation stage identifies potential software defects before code execution, thereby reducing debugging time and lowering the cost of addressing issues later in development. The elaborated system represents a crucial step towards safer and more dependable Cyber-Physical System applications. This approach allows us to identify approximately 90% of incorrect usage of program variables; additionally, it detects over 50% of erroneous operations during compilation and execution of large-scale programs in real-world conditions. Conclusions. Scientific novelty: it proposed and developed a specialized C++-type library for formal compile-time software verification of Cyber-Physical Systems software. The proposed C++-type library leverages dimensional and orientational analysis to enhance software quality, reliability, and real-time formal verification. Although the proposed method for formal verification is not tailor-made for cyber-physical objects and systems, given its primary focus on software-level concerns, it does exhibit adaptability for verifying general-purpose software that incorporates various physical parameters. This versatility extends to diverse domains such as educational, gaming, and simulation software.

Keywords


Cyber-Physical Systems; dimensional analysis; formal verification; orientational analysis; software quality; type system

Full Text:

PDF

References


Vasylenko, O., Ivchenko, S., & Snizhnoi, H. Design of information and measurement systems within the Industry 4.0 paradigm. Radioelectronic and Computer Systems, 2023, no. 1, pp. 45-54. DOI: 10.32620/reks.2023.1.04.

Valette, E., El-Haouzi, H. B., & Demesure, G. Industry 5.0 and its technologies: A systematic literature review upon the human place into IoT - and CPS-based industrial systems. Computers & Industrial Engineering, 2023, vol. 184. DOI: 10.1016/j.cie.2023.109426.

Schneider, G. F., Wicaksono, H., Ovtcharova, J. Virtual engineering of cyber-physical automation systems: The case of control logic. Advanced engineering informatics, 2019, no. 39, pp. 127-143. DOI: 10.1016/j.aei.2018.11.009.

Manzos, Y., Sokolova, Y. The method of data compression in Internet of Things communication. Radioelectronic and Computer Systems, 2020, no. 4, pp. 57-67. DOI:10.32620/reks.2020.4.05 (In Ukrainian)

Olaniyi, O., Okunleye, O. J., & Olabanji, S. O. Advancing Data-Driven Decision-Making in Smart Cities through Big Data Analytics: A Comprehensive Review of Existing Literature. Current Journal of Applied Science and Technology, 2023, vol. 42, iss. 25, pp. 10-18. DOI: 10.9734/CJAST/2023/v42i254181.

Maskuriy, R., Selamat, A., Ali, KN., Maresova, P., & Krejcar, O. Industry 4.0 for the Construction Industry – How Ready Is the Industry? Applied Sciences, 2019, vol. 9, no.14, article no. 2819. DOI: 10.3390/app9142819.

Miśkiewicz, R., & Wolniak, R. Practical Application of the Industry 4.0 Concept in a Steel Company. Sustainability, 2020, vol. 12, no. 14, article no. 5776. DOI: 10.3390/su12145776.

Mane, V. Environmental Monitoring Using Internet of Things. International Journal of Electrical and Computer Engineering, 2022, vol. 11, iss. 1, pp. 2-9. DOI: 10.15662/IJAREEIE.2022.1101015.

Rayan, R.A., Tsagkaris, C., & Iryna, R. B. The Internet of Things for Healthcare: Applications, Selected Cases and Challenges. IoT in Healthcare and Ambient Assisted Living. Studies in Computational Intelligence, 2021, vol. 933, pp. 1-15. DOI: 10.1007/978-981-15-9897-5_1.

Strelkina, А. Information technology for dependability assessment and providing of healthcare IoT systems. Radioelectronic and Computer Systems, 2019, no. 3, pp. 48-54. DOI:10.32620/reks.2019.3.05. (In Ukrainian).

Syed, A. S., Sierra-Sosa, D., Kumar, A., & Elmaghraby, A. IoT in Smart Cities: A Survey of Technologies, Practices and Challenges. Smart Cities, 2021, no. 4(2), pp. 429-475. DOI: 10.3390/smartcities4020024.

Deepak, V., Mishra, A., & Mishra, K. Role of IOT in introducing Smart Agriculture. International Research. Journal of Engineering and Technology (IRJET), 2022, no. 9, pp. 883-887.

Mourtzis, D., Vlachou, K., Dimitrakopoulos, G., & Zogopoulos, V. Cyber-Physical Systems and Education 4.0 – The Teaching Factory 4.0 Concept. Procedia Manufacturing, 2018, no. 23, pp. 129-134. DOI: 10.1016/j.promfg.2018.04.005.

Tsiatsis, V., Karnouskos, S., Höller, J., Boyle, D., & Mulligan, C. Chapter 16 - Autonomous Vehicles and Systems of Cyber-Physical Systems. Internet of Things, 2019, pp. 299-305. DOI: 10.1016/B978-0-12-814435-0.00029-8.

Alsulami, A. A., Abu Al-Haija, Q., Alturki, B., Alqahtani, A., & Alsini, R. Security Strategy for Autonomous Vehicle Cyber-Physical Systems Using Transfer Learning. Journal of Cloud Computing, 2023, vol. 12, article no. 181. DOI: 10.21203/rs.3.rs-2301648/v1.

Banerjee, A., Maity, A., Gupta S. K., & Lamrani, I. Statistical Conformance Checking of Aviation Cyber-Physical Systems by Mining Physics Guided Models. Proceedings of the 2023 Aerospace Conference, Big Sky, MT, USA, IEEE, 2023, pp. 1-8, DOI: 10.1109/AERO55745.2023.10115613.

Manzhos, Y., & Sokolova, Y. A Method of IoT Information Compression. International Journal of Computing, 2022, vol. 21, iss. 1, pp. 100-110. DOI: 10.47839/ijc.21.1.2523.

Fursov, I., Yamkovyi, K., & Shmatko, O. Smart Grid and wind generators: an overview of cyber threats and vulnerabilities of power supply networks. Radioelectronic and Computer Systems, 2022, no. 4, pp. 50-63. DOI: 10.32620/reks.2022.4.04.

Smadi, A. A., Ajao, B. T., Johnson, B. K., Lei, H., Chakhchoukh, Y., & Abu Al-Haija, Q. A Comprehensive Survey on Cyber-Physical Smart Grid Testbed Architectures: Requirements and Challenges. Electronics, 2021, vol. 10, no. 9, article no. 1043. DOI: 10.3390/electronics10091043.

Kang, B., Seo, K.-M., & Kim, T. G. Model-Based Design of Defense Cyber-Physical Systems to Analyze Mission Effectiveness and Network Performance. IEEE Access, 2019, vol. 7, no. 1, pp. 42063-42080. DOI: 10.1109/ACCESS.2019.2907566.

Wisniewski, R., Bazydło, G., Szcześniak, P., Grobelna, I., & Wojnakowski, M. Design and Verification of Cyber-Physical Systems Specified by Petri Nets – A Case Study of a Direct Matrix Converter. Mathematics, 2019, vol. 7, no. 9, article no. 812. DOI: 10.3390/math7090812.

Cordeiro, L. C., de Lima Filho, E. B., & Bessa, I. V. Survey on automated symbolic verification and its application for synthesizing cyber-physical systems. IET Cyber-Physical Systems: Theory & Applications, 2019, vol. 5, iss. 1, pp. 1-24. DOI: 10.1049/iet-cps.2018.5006.

Grobelna, I., Wiśniewski, R., & Wojnakowski, M. Specification of Cyber-Physical Systems with the Application of Interpreted Nets. Proceedings of the IECON 2019 - 45th Annual Conference of the IEEE Industrial Electronics Society, Lisbon, Portugal, IEEE, 2019, pp. 5887-5891. DOI: 10.1109/IECON.2019.8926908.

Luckeneder, C., & Kaindl, H. A case study of systematic top-down design of cyber-physical models with integrated validation and formal verification. Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing (SAC '19). Association for Computing Machinery, New York, NY, USA, 2019, pp. 1828-1836. DOI: 10.1145/3297280.3297460.

Bernardeschi, C., Domenici, A., & Saponara, S. Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-physical Systems. Electronic Communications of the EASST, 2019, vol. 77, pp. 1–9. DOI: 10.14279/tuj.eceasst.77.1106.1050.

Misson, H. A., Gonçalves F. S., & Becker, L. B. Applying Integrated Formal Methods on CPS Design, Proceedings of the IX Brazilian Symposium on Computing Systems Engineering (SBESC), Natal, Brazil, 2019, pp. 1-8. DOI: 10.1109/SBESC49506.2019.9046084.

Grobelna, I. Formal Verification of Control Modules in Cyber-Physical Systems. Sensors, 2020, vol. 20, no.18, article no. 5154. DOI: 10.3390/s20185154.

Garro, A., Vaccaro, V., Dutré, S., & Stegen, J. Cyber-Physical Systems engineering: model-based solutions. Proceedings of the SummerSim-SCSC 2019, Berlin, Germany, 2019, Society for Modeling and Simulation International (SCS). Available at: https://scs.org/wp-content/uploads/2020/02/CYBER-PHYSICAL-SYSTEMS-ENGINEERING-MODEL-BASED-SOLUTIONS.pdf (accessed 24 July 2019).

Wisniewski, R., Bazydło, G., Szcześniak, P., Grobelna, I., & Wojnakowski, M. Design and Verification of Cyber-Physical Systems Specified by Petri Nets – A Case Study of a Direct Matrix Converter. Mathematics, 2019, vol. 7, no. 9, article no. 812. DOI: 10.3390/math7090812.

Nikolakis, N., Maratos, V., & Makris, S. A Cyber-Physical System (CPS) approach for safe human-robot collaboration in a shared workplace. Robotics and Computer-Integrated Manufacturing, 2019, vol. 56, pp. 233-243. DOI: 10.1016/j.rcim.2018.10.003.

The Incredible Story of the Gimli Glider. Simple Flying. Available at: https://thedailywtf.com/articles/the-therac-25-incident (accessed 6 August 2023).

The Patriot Missile Failure. Available at: https://www-users.cse.umn.edu/~arnold/disasters/patriot.html (accessed 23 August 2000).

Stephenson, A. G., LaPiana, L. S.; Mulville, D. R., Rutledge, P. J., Bauer, F. H., Folta, D., Dukeman, G. A., Sackheim, R., & Norvig, P. Mars Climate Orbiter Mishap Investigation Board Phase I Report NASA. Available at: chrome-extension://efaidnbmnnnibpcajpcglclefindmkaj/https://llis.nasa.gov/llis_lib/pdf/1009464main1_0641-mr.pdf. (accessed 10 November 1999).

Hall, B. Software representation of measured physical quantities. Series on Advanced in Mathematics for Applied Sciences. Advanced Mathematical and Computational Tools in Metrology and Testing XII, 2021, vol. 90, pp. 273-284. DOI: 10.1142/9789811242380_0016.

Manzhos, Y., & Sokolova, Y. A Software Verification Method for the Internet of Things and Cyber-Physical Systems. Computation, 2023, no. 11 (7), article no. 135. DOI: 10.3390/computation11070135.

Schabel, M. C., & Watanabe, S. Chapter 42. Boost.Units 1.1.0. Available at: https://www.boost.org/doc/libs/1_83_0/doc/html/boost_units.html. (accessed 17 August 2003).

Benri is a C++ library for compile time checking of physical quantities. Available at: https://github.com/jansende/benri (accessed 4 October 2019).

Pusz, M. A C++ Approach to Physical Units. Available at: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p1935r2.html#biblio-nic_units (accessed 13 January 2020).

Moene, M., Huebl, A., Reinhold, S., & Pilz, T. PhysUnits-CT-Cpp11 (compile time). Available at: https://github.com/martinmoene/PhysUnits-CT-Cpp11. (accessed 24 May 2020).

Eigen is a C++ template library for linear algebra: matrices, vectors, numerical solvers, and related algorithms. Available at: https://eigen.tuxfamily.org/index.php?title=Main_Page. (accessed 18 August 2021).

OpenGl Mathematics (GLM). Available at: Available at: https://github.com/g-truc/glm (accessed 13 April 2020).

Weige, M. Quaternion Library for C. Available at: https://github.com/MartinWeigel/Quaternion (accessed 16 May 2022).

Mahoney, J. F. Dimensional Analysis. Procedia Manufacturing, 2019, vol. 38, pp. 694-701. DOI: 10.1016/j.promfg.2020.01.094.

McKeever, S. Unit of measurement libraries, their popularity and suitability. Software: Practice and Experience, 2021, vol. 51, iss. 4, pp. 711-734. DOI: 10.1002/spe.2926.

McKeever, S. Acknowledging Implementation Trade-Offs When Developing with Units of Measurement. Communications in Computer and Information Science, 2023, vol. 1708, pp. 25-47. DOI: 10.1007/978-3-031-38821-7_2.

Siano, D. B. Orientational Analysis – A Supplement to Dimensional Analysis. Journal of the Franklin Institute, 1985, vol. 320, iss. 6, pp. 267-283. DOI: 10.1016/0016-0032(85)90031-6.

Siano, D. B. Orientational analysis, tensor analysis and the group properties of the SI supplementary units. Journal of the Franklin Institute, 1985, vol. 320, iss. 6, pp. 285-302. DOI: 10.1016/0016-0032(85)90032-8.

Dos Santos, L. F. Orientational Analysis of the Vesic’s Bearing Capacity of Shallow Foundations. Soils Rocks, 2020, vol. 43, pp. 3-9. DOI: 10.28927/SR.431003.

Sutter, H. Metaclasses: Generative C++. Available at: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0707r3.pdf. (accessed 11 February 2018).

Sutton, A. Metaprogramming. Available at: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p2237r0.pdf. (accessed 15 October 2020).

Working Draft, Standard for Programming Language C++. Available at: https://isocpp.org/files/papers/N4928.pdf. (accessed 22 May 2023).




DOI: https://doi.org/10.32620/reks.2024.1.11

Refbacks

  • There are currently no refbacks.