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

Roopak Sinha, Sandeep Patil, Luis Gomes, Valeriy Vyatkin

Research output: Contribution to journalReview article

2 Citations (Scopus)

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.

Original languageEnglish
Article number8678839
Pages (from-to)3772-3783
Number of pages12
JournalIEEE Transactions on Industrial Informatics
Volume15
Issue number7
DOIs
Publication statusPublished - 1 Jul 2019

Fingerprint

Formal methods
Life cycle
Automation
Requirements engineering
Systems analysis
Testing

Keywords

  • Formal methods
  • formal verification
  • IEC 61131
  • IEC 61499
  • industrial automation systems (IAS)
  • industrial control

Cite this

Sinha, Roopak ; Patil, Sandeep ; Gomes, Luis ; Vyatkin, Valeriy. / A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems. In: IEEE Transactions on Industrial Informatics. 2019 ; Vol. 15, No. 7. pp. 3772-3783.
@article{3b301fd18d314f5fb2937ec6bb70c989,
title = "A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems",
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.",
keywords = "Formal methods, formal verification, IEC 61131, IEC 61499, industrial automation systems (IAS), industrial control",
author = "Roopak Sinha and Sandeep Patil and Luis Gomes and Valeriy Vyatkin",
note = "Sem PDF conforme despacho",
year = "2019",
month = "7",
day = "1",
doi = "10.1109/TII.2019.2908665",
language = "English",
volume = "15",
pages = "3772--3783",
journal = "IEEE Transactions on Industrial Informatics",
issn = "1551-3203",
publisher = "IEEE",
number = "7",

}

A Survey of Static Formal Methods for Building Dependable Industrial Automation Systems. / Sinha, Roopak; Patil, Sandeep; Gomes, Luis; Vyatkin, Valeriy.

In: IEEE Transactions on Industrial Informatics, Vol. 15, No. 7, 8678839, 01.07.2019, p. 3772-3783.

Research output: Contribution to journalReview article

TY - JOUR

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

AU - Sinha, Roopak

AU - Patil, Sandeep

AU - Gomes, Luis

AU - Vyatkin, Valeriy

N1 - Sem PDF conforme despacho

PY - 2019/7/1

Y1 - 2019/7/1

N2 - 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.

AB - 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.

KW - Formal methods

KW - formal verification

KW - IEC 61131

KW - IEC 61499

KW - industrial automation systems (IAS)

KW - industrial control

UR - http://www.scopus.com/inward/record.url?scp=85068606764&partnerID=8YFLogxK

U2 - 10.1109/TII.2019.2908665

DO - 10.1109/TII.2019.2908665

M3 - Review article

VL - 15

SP - 3772

EP - 3783

JO - IEEE Transactions on Industrial Informatics

JF - IEEE Transactions on Industrial Informatics

SN - 1551-3203

IS - 7

M1 - 8678839

ER -