SITL-Based Formal Verification of Cyber-Physical Systems Software: Reliability Model, Method and Implementation

This study focuses on developing of a software verification method using SI (The International System of Units) - based Template Libraries (TL). It analyses and enhances the reliability of cyber-physical systems (CPS) and IoT software by addressing SI prefixes, units, and orientation errors in C/C++ programs without increasing memory usage. Such errors often go undetected by conventional methods, leading to critical issues. Inspired by Siano’s approach, the study extends the SI to include orientation metrics. The technique leverages C++ metaprogramming to enforce the correct use of SI units and prefixes through dimensional and orientational analysis, enabling precise control of physical object rotations. A reliable SI unit model was developed, demonstrating the advantages of the extended system. Verifying dimensions and orientations at compile-time allows early detection of potential software defects, reducing debugging time and costs. The SI-based template library enhances software safety and reliability, identifying 90% of incorrect variable usage and over 50% of erroneous operations in large-scale programs. It was validated through development and integration Euler's differential equations and formal software verification of CPS. This SITL-based approach significantly advances software development, improving compile-time and run-time verification across domains such as manufacturing, transport, space and other systems.