A Survey on Formal Verification Approaches for Dependable Systems

TL;DR

This survey reviews formal verification methods used in the development of dependable digital embedded systems, emphasizing their importance in ensuring safety and correctness in safety-critical applications.

Contribution

It provides a comprehensive overview of formal verification approaches and discusses their application in enhancing system dependability.

Findings

Formal methods are increasingly adopted in safety-critical system verification.

Various formal verification techniques offer different trade-offs in complexity and coverage.

Formal V&V methods significantly improve system dependability and early error detection.

Abstract

The complexity of digital embedded systems has been increasing in different safety-critical applications such as industrial automation, process control, transportation, and medical digital devices. The correct operation of these systems relies too heavily on the behavior of the embedded digital device. As a result, any mistake or error made during the design stage of the embedded device can change the overall functionality of the critical system and cause catastrophic consequences. To detect these errors and eliminate their effects on the system, new error detection approaches must be innovated and used in the design of the digital system. However, these methods require enormous costs and time. One of these methods being employed to solve this issue is called Verification and Validation (V&V) which confirms that the system behavior meets the requirements early in the development process, before moving on to the implementation phase. Because of their benefits and importance in the building of complex digital systems, the employment of formal V&V methods has recently attracted a lot of attention. This paper focuses on presenting various studies on formal verification approaches and how the V&V can be achieved for developing high dependable digital embedded systems