Formal Verification of Safety and Security Properties in Industry 4.0 Applications

With the advent of Industry 4.0 (I4.0) systems, ensuring the safety and security of these systems' design has become a paramount concern for stakeholders. One concern is the increased costs of fixing errors in later phases, such as integration and operation compared to the design phase. Formal verification techniques offer a rigorous approach to verifying the correctness of system behaviours and properties. This paper explains the fundamental principles of formal verification in safety and security domains. We use a SysML-based environment called AVATAR ("Automated Verification of Real Time Software"). It allows for a formal description and verification of safety and security properties. Specifically, we demonstrate the application of AVATAR in verifying the safety and security properties of a Cobot system architecture upon requirements. Moreover, we evaluate the challenges, opportunities, and limitations of using AVATAR in industrial settings and provide recommendations for its enhancement or designing a new methodology for I4.0 application verification. The results show that formal verification techniques can be enhanced to address safety and security concerns in I4.0 complex and critical systems.