Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • 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å tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap. Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.ORCID-id: 0000-0002-9315-9920
2024 (engelsk)Inngår i: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 216, artikkel-id 112153Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
Elsevier, 2024. Vol. 216, artikkel-id 112153
Emneord [en]
Formal specifications, Formal verification, Instrumentation and control, Model checking, Requirements engineering
HSV kategori
Forskningsprogram
Kommunikations- och beräkningssystem
Identifikatorer
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
Merknad

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

Fulltext licenes: CC BY

Tilgjengelig fra: 2024-08-01 Laget: 2024-08-01 Sist oppdatert: 2024-11-20bibliografisk kontrollert

Open Access i DiVA

fulltext(1800 kB)53 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 1800 kBChecksum SHA-512
144797715e7514c21f9108c3d006f77ba42905f30c1c62cb4b4ea717586f81907a14999ca6b673b6689e8707a0b17bf982aa4c2a19244c919af3248eec2bcf23
Type fulltextMimetype application/pdf

Andre lenker

Forlagets fulltekstScopus

Person

Vyatkin, Valeriy

Søk i DiVA

Av forfatter/redaktør
Pakonen, AnttiVyatkin, Valeriy
Av organisasjonen
I samme tidsskrift
Journal of Systems and Software

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 53 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 244 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf