Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Evaluation of visual property specification languages based on practical model-checking experience
VTT Technical Research Centre of Finland Ltd., Espoo, Finland.ORCID iD: 0000-0002-6803-2303
IPRally Technologies Oy, Helsinki, Finland.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.ORCID iD: 0000-0002-9315-9920
2024 (English)In: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 216, article id 112153Article in journal (Refereed) Published
Abstract [en]

Formal verification methods like model checking can provide mathematical proofs of design correctness, so their use is justified in applications where safety or reliability requirements are high. A key challenge for the wider adoption of model checking is the effort and expertise needed in formalizing functional requirements into verifiable properties. A particular challenge in specifying formal properties for industrial instrumentation and control (I&C) logics is accounting for the sequencing and timing issues that arise from, e.g., the dynamic behavior of the plant being controlled. In this paper, we evaluate different visual property specification languages that are aimed at making formal methods more accessible. We have collected 3923 formal properties from practical model checking projects in the nuclear and rail traffic industries and identified the most commonly occurring types of properties. Based on the sample data, a real-world example logic, and our practical experience, we identify requirements for a user-friendly property specification language most suited for our specific domain of industrial I&C.

Place, publisher, year, edition, pages
Elsevier, 2024. Vol. 216, article id 112153
Keywords [en]
Formal specifications, Formal verification, Instrumentation and control, Model checking, Requirements engineering
National Category
Computer Sciences Computer Systems Software Engineering
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-108427DOI: 10.1016/j.jss.2024.112153ISI: 001274706300001Scopus ID: 2-s2.0-85198959721OAI: oai:DiVA.org:ltu-108427DiVA, id: diva2:1886444
Note

Validerad;2024;Nivå 2;2024-08-01 (signyg);

Fulltext licenes: CC BY

Available from: 2024-08-01 Created: 2024-08-01 Last updated: 2024-11-20Bibliographically approved

Open Access in DiVA

fulltext(1800 kB)51 downloads
File information
File name FULLTEXT01.pdfFile size 1800 kBChecksum SHA-512
144797715e7514c21f9108c3d006f77ba42905f30c1c62cb4b4ea717586f81907a14999ca6b673b6689e8707a0b17bf982aa4c2a19244c919af3248eec2bcf23
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records

Vyatkin, Valeriy

Search in DiVA

By author/editor
Pakonen, AnttiVyatkin, Valeriy
By organisation
Computer Science
In the same journal
Journal of Systems and Software
Computer SciencesComputer SystemsSoftware Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 51 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 242 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf