kth.sePublications
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
VrFy: Verification of Formal Requirements using Generic Traces
Eindhoven Univ Technol, Eindhoven, Netherlands..ORCID iD: 0000-0003-4918-5344
KTH, School of Electrical Engineering and Computer Science (EECS), Electrical Engineering, Electronics and Embedded systems.ORCID iD: 0000-0002-1277-3903
Bombardier Transportat Sweden AB, Stockholm, Sweden..
Bombardier Transportat Sweden AB, Stockholm, Sweden..
2021 (English)In: 2021 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY COMPANION (QRS-C 2021), Institute of Electrical and Electronics Engineers (IEEE) , 2021, p. 177-183Conference paper, Published paper (Refereed)
Abstract [en]

In order to fulfil standards governing the development of safety-critical systems, requirements are often shown to be satisfied by means of traditional techniques such as system analysis and testing activities. While these techniques have been used for many years, issues can still arise due to weak tests, not fully covering all requirement scenarios; and due to misinterpretation of requirements, leading to futile test activities. Having simpler techniques to show that requirements are properly fulfilled and that depend less on thoroughness of the tester is beneficial. To tackle these issues, we present an analysis method together with an accompanying toolset, VrFy, implementing a novel technique to automate the detection of violations of requirements. Monitors are generated automatically, and the risk due to misinterpretation of requirements is reduced by using a formal notation (LTL3). Compared to related work, the proposed technique is programming language agnostic and can identify the exact time when requirements are violated, supporting the end user to quickly spot the root cause. By means of a real-world use case in the railway domain, we show how the tool can be used to augment traditional verification techniques.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2021. p. 177-183
Series
IEEE International Conference on Software Quality, Reliability and Security Companion, ISSN 2693-938X
Keywords [en]
Trace Validation, LTL3, NBA, Programming Language Agnostic, Railway Domain, Trace Compass
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:kth:diva-315462DOI: 10.1109/QRS-C55045.2021.00034ISI: 000808814500024Scopus ID: 2-s2.0-85140926486OAI: oai:DiVA.org:kth-315462DiVA, id: diva2:1681711
Conference
21st IEEE International Conference on Software Quality, Reliability and Security (QRS), 6-10 December, 2021, Hainan, China
Note

Part of proceedings: ISBN 978-1-6654-7836-6

QC 20220707

Available from: 2022-07-07 Created: 2022-07-07 Last updated: 2023-06-08Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Jordao, Rodolfo

Search in DiVA

By author/editor
Olthuis, Jorrit J.Jordao, Rodolfo
By organisation
Electronics and Embedded systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 63 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