A Comparison of Formal Verification Approaches for IEC 61499

Jan Olaf Blech; Per Lindgren; David Pereira; Valeriy Vyatkin; Alois Zoitl

doi:10.1109/ETFA.2016.7733636

A Comparison of Formal Verification Approaches for IEC 61499

Jan Olaf Blech
, Per Lindgren
, David Pereira
, Valeriy Vyatkin
, Alois Zoitl

Royal Melbourne Institute of Technology University
Luleå University of Technology
Polytechnic Institute of Porto
Fortiss GmbH

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

12 Citations (Scopus)

Abstract

Engineering and computer science have come up with a variety of techniques to increase the confidence in systems, increase reliability, facilitate certification, improve reuse and maintainability, improve interoperability and portability. Among them are various techniques based on formal models to enhance testing, validation and verification. In this paper, we are concentrating on formal verification both at runtime and design time of a system. Formal verification of a system property at design time is the process of mathematically proving that the property indeed holds. At runtime, one can check the validity of the property and report deviations by monitoring the system execution. Formal verification relies on semantic models, descriptions of the system and its properties. We report on ongoing verification work and present two different approaches for formal verification of IEC 61499-based programs. We provide two examples of ongoing work to exemplify the design and the runtime verification approaches.

Original language	English
Title of host publication	2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016
Publisher	IEEE
Number of pages	4
Volume	2016-November
ISBN (Electronic)	9781509013142
DOIs	https://doi.org/10.1109/ETFA.2016.7733636
Publication status	Published - 3 Nov 2016
MoE publication type	A4 Conference publication
Event	IEEE International Conference on Emerging Technologies and Factory Automation - Berlin, Germany Duration: 6 Sept 2016 → 9 Sept 2016 Conference number: 21 http://www.etfa2016.org/

Publication series

Name	IEEE International Conference on Emerging Technologies and Factory Automation-ETFA
Publisher	IEEE
ISSN (Print)	1946-0740

Conference

Conference	IEEE International Conference on Emerging Technologies and Factory Automation
Abbreviated title	EFTA
Country/Territory	Germany
City	Berlin
Period	06/09/2016 → 09/09/2016
Internet address	http://www.etfa2016.org/

Access to Document

10.1109/ETFA.2016.7733636

Cite this

Blech, J. O., Lindgren, P., Pereira, D., Vyatkin, V., & Zoitl, A. (2016). A Comparison of Formal Verification Approaches for IEC 61499. In 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016 (Vol. 2016-November). Article 7733636 (IEEE International Conference on Emerging Technologies and Factory Automation-ETFA). IEEE. https://doi.org/10.1109/ETFA.2016.7733636

@inproceedings{f986b4a2eadc426aac44701ebac65146,

title = "A Comparison of Formal Verification Approaches for IEC 61499",

abstract = "Engineering and computer science have come up with a variety of techniques to increase the confidence in systems, increase reliability, facilitate certification, improve reuse and maintainability, improve interoperability and portability. Among them are various techniques based on formal models to enhance testing, validation and verification. In this paper, we are concentrating on formal verification both at runtime and design time of a system. Formal verification of a system property at design time is the process of mathematically proving that the property indeed holds. At runtime, one can check the validity of the property and report deviations by monitoring the system execution. Formal verification relies on semantic models, descriptions of the system and its properties. We report on ongoing verification work and present two different approaches for formal verification of IEC 61499-based programs. We provide two examples of ongoing work to exemplify the design and the runtime verification approaches.",

author = "Blech, \{Jan Olaf\} and Per Lindgren and David Pereira and Valeriy Vyatkin and Alois Zoitl",

year = "2016",

month = nov,

day = "3",

doi = "10.1109/ETFA.2016.7733636",

language = "English",

volume = "2016-November",

series = "IEEE International Conference on Emerging Technologies and Factory Automation-ETFA",

publisher = "IEEE",

booktitle = "2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016",

address = "United States",

note = "IEEE International Conference on Emerging Technologies and Factory Automation, EFTA ; Conference date: 06-09-2016 Through 09-09-2016",

url = "http://www.etfa2016.org/",

}

Blech, JO, Lindgren, P, Pereira, D, Vyatkin, V & Zoitl, A 2016, A Comparison of Formal Verification Approaches for IEC 61499. in 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016. vol. 2016-November, 7733636, IEEE International Conference on Emerging Technologies and Factory Automation-ETFA, IEEE, IEEE International Conference on Emerging Technologies and Factory Automation, Berlin, Germany, 06/09/2016. https://doi.org/10.1109/ETFA.2016.7733636

A Comparison of Formal Verification Approaches for IEC 61499. / Blech, Jan Olaf; Lindgren, Per; Pereira, David et al.
2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016. Vol. 2016-November IEEE, 2016. 7733636 (IEEE International Conference on Emerging Technologies and Factory Automation-ETFA).

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

TY - GEN

T1 - A Comparison of Formal Verification Approaches for IEC 61499

AU - Blech, Jan Olaf

AU - Lindgren, Per

AU - Pereira, David

AU - Vyatkin, Valeriy

AU - Zoitl, Alois

N1 - Conference code: 21

PY - 2016/11/3

Y1 - 2016/11/3

N2 - Engineering and computer science have come up with a variety of techniques to increase the confidence in systems, increase reliability, facilitate certification, improve reuse and maintainability, improve interoperability and portability. Among them are various techniques based on formal models to enhance testing, validation and verification. In this paper, we are concentrating on formal verification both at runtime and design time of a system. Formal verification of a system property at design time is the process of mathematically proving that the property indeed holds. At runtime, one can check the validity of the property and report deviations by monitoring the system execution. Formal verification relies on semantic models, descriptions of the system and its properties. We report on ongoing verification work and present two different approaches for formal verification of IEC 61499-based programs. We provide two examples of ongoing work to exemplify the design and the runtime verification approaches.

AB - Engineering and computer science have come up with a variety of techniques to increase the confidence in systems, increase reliability, facilitate certification, improve reuse and maintainability, improve interoperability and portability. Among them are various techniques based on formal models to enhance testing, validation and verification. In this paper, we are concentrating on formal verification both at runtime and design time of a system. Formal verification of a system property at design time is the process of mathematically proving that the property indeed holds. At runtime, one can check the validity of the property and report deviations by monitoring the system execution. Formal verification relies on semantic models, descriptions of the system and its properties. We report on ongoing verification work and present two different approaches for formal verification of IEC 61499-based programs. We provide two examples of ongoing work to exemplify the design and the runtime verification approaches.

UR - https://www.scopus.com/pages/publications/84996483346

U2 - 10.1109/ETFA.2016.7733636

DO - 10.1109/ETFA.2016.7733636

M3 - Conference article in proceedings

AN - SCOPUS:84996483346

VL - 2016-November

T3 - IEEE International Conference on Emerging Technologies and Factory Automation-ETFA

BT - 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016

PB - IEEE

T2 - IEEE International Conference on Emerging Technologies and Factory Automation

Y2 - 6 September 2016 through 9 September 2016

ER -

Blech JO, Lindgren P, Pereira D, Vyatkin V, Zoitl A. A Comparison of Formal Verification Approaches for IEC 61499. In 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016. Vol. 2016-November. IEEE. 2016. 7733636. (IEEE International Conference on Emerging Technologies and Factory Automation-ETFA). doi: 10.1109/ETFA.2016.7733636

A Comparison of Formal Verification Approaches for IEC 61499

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this