Evaluation of visual property specification languages based on practical model-checking experience
Loading...
Access rights
openAccess
publishedVersion
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Date
Major/Subject
Mcode
Degree programme
Language
en
Pages
18
Series
Journal of Systems and Software, Volume 216, pp. 1-18
Abstract
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.Description
Publisher Copyright: © 2024 The Authors
Other note
Citation
Pakonen, A, Buzhinsky, I & Vyatkin, V 2024, 'Evaluation of visual property specification languages based on practical model-checking experience', Journal of Systems and Software, vol. 216, 112153, pp. 1-18. https://doi.org/10.1016/j.jss.2024.112153