A Survey on Formal Verification Approaches for Dependable Systems

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