User-friendly formal specification languages - Conclusions drawn from industrial experience on model checking

Antti Pakonen, Cheng Pang, Igor Buzhinsky, Valeriy Vyatkin

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

13 Citations (Scopus)

Abstract

Formal methods - such as model checking - have definite advantages over more commonplace verification techniques. By providing proof of the analyzed systems' correctness, they are especially useful in domains that are under regulatory supervision, like the nuclear industry. The foremost challenge for wider adoption of model checking is the effort and the expertise required for formalizing functional requirements into verifiable properties. A particular challenge in verifying the application software of industrial process control systems is taking into account the different sequencing and timing issues that arise from, e.g., the dynamic behavior of the plant processes being controlled. In this paper, we review specification languages that are aimed at making formal methods more accessible. We have collected 1079 sample formal properties from practical model checking projects in the nuclear industry, and identified repeatedly occurring property types. We present our findings, and based on the sample data, evaluate the applicability of different approaches on user-friendly property specification.

Original languageEnglish
Title of host publicationProceedings of the 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016
PublisherIEEE
Volume2016-November
ISBN (Electronic)9781509013142
DOIs
Publication statusPublished - 3 Nov 2016
MoE publication typeA4 Article in a conference publication
EventIEEE International Conference on Emerging Technologies and Factory Automation - Berlin, Germany
Duration: 6 Sep 20169 Sep 2016
Conference number: 21
http://www.etfa2016.org/

Publication series

NameIEEE International Conference on Emerging Technologies and Factory Automation-ETFA
PublisherIEEE
ISSN (Print)1946-0740

Conference

ConferenceIEEE International Conference on Emerging Technologies and Factory Automation
Abbreviated titleEFTA'2016
CountryGermany
CityBerlin
Period06/09/201609/09/2016
Internet address

Keywords

  • formal specification languages
  • model checking
  • nuclear power
  • requirement patterns
  • requirements engineering

Fingerprint Dive into the research topics of 'User-friendly formal specification languages - Conclusions drawn from industrial experience on model checking'. Together they form a unique fingerprint.

  • Cite this

    Pakonen, A., Pang, C., Buzhinsky, I., & Vyatkin, V. (2016). User-friendly formal specification languages - Conclusions drawn from industrial experience on model checking. In Proceedings of the 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation, ETFA 2016 (Vol. 2016-November). [7733717] (IEEE International Conference on Emerging Technologies and Factory Automation-ETFA). IEEE. https://doi.org/10.1109/ETFA.2016.7733717