Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat 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 (Engelska)Ingår i: Journal of Systems and Software, ISSN 0164-1212, E-ISSN 1873-1228, Vol. 216, artikel-id 112153Artikel i tidskrift (Refereegranskat) 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.

Ort, förlag, år, upplaga, sidor
Elsevier, 2024. Vol. 216, artikel-id 112153
Nyckelord [en]
Formal specifications, Formal verification, Instrumentation and control, Model checking, Requirements engineering
Nationell ämneskategori
Datavetenskap (datalogi) Datorsystem Programvaruteknik
Forskningsämne
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
Anmärkning

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

Fulltext licenes: CC BY

Tillgänglig från: 2024-08-01 Skapad: 2024-08-01 Senast uppdaterad: 2024-11-20Bibliografiskt granskad

Open Access i DiVA

fulltext(1800 kB)53 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 1800 kBChecksumma SHA-512
144797715e7514c21f9108c3d006f77ba42905f30c1c62cb4b4ea717586f81907a14999ca6b673b6689e8707a0b17bf982aa4c2a19244c919af3248eec2bcf23
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltextScopus

Person

Vyatkin, Valeriy

Sök vidare i DiVA

Av författaren/redaktören
Pakonen, AnttiVyatkin, Valeriy
Av organisationen
Datavetenskap
I samma tidskrift
Journal of Systems and Software
Datavetenskap (datalogi)DatorsystemProgramvaruteknik

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 53 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 244 träffar
RefereraExporteraLänk till posten
Permanent länk

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