A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems

TL;DR

This survey reviews static formal methods applied in various phases of the system development life cycle to enhance the dependability of industrial automation systems, highlighting current approaches and future research directions.

Contribution

It categorizes existing static formal methods across SDLC phases, identifying gaps and proposing future research directions for dependable industrial automation systems.

Findings

Static formal methods are effectively used in requirements engineering, design, verification, and maintenance.

Research gaps exist in applying formal methods to certain SDLC phases.

Future directions include integrating formal methods more seamlessly into industrial processes.

Abstract

Industrial automation systems (IAS) need to be highly dependable; they should not merely function as expected but also do so in a reliable, safe, and secure manner. Formal methods are mathematical techniques that can greatly aid in developing dependable systems and can be used across all phases of the system development life cycle (SDLC), including requirements engineering, system design and implementation, verification and validation (testing), maintenance, and even documentation. This state-of-the-art survey reports existing formal approaches for creating more dependable IAS, focusing on static formal methods that are used before a system is completely implemented. We categorize surveyed works based on the phases of the SDLC, allowing us to identify research gaps and promising future directions for each phase.