mdh.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
Automated SMT-based Consistency Checking of Industrial Critical Requirements
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-4987-7669
Scania AB CV, Södertälje, Sweden.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
2017 (English)In: ACM SIGAPP Applied Computing Review, ISSN 1559-6915, E-ISSN 1931-0161, Vol. 17, no 4, p. 15-28Article in journal (Refereed) Published
Abstract [en]

With the ever-increasing size, complexity and intricacy of system requirements specifications, it becomes difficult to ensure their correctness with respect to certain criteria such as consistency. Automated formal techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. Sometimes such techniques incur a high modeling cost or analysis time, or are not applicable. To address such problems, in this paper we propose an automated consistency analysis technique of requirements that are formalized based on patterns, and checked using state-of-the-art Satisfiability Modulo Theories solvers. Our method assumes several transformation steps, from textual requirements to formal logic, and next into the format suited for the SMT tool. To automate such steps, we propose a tool, called PROPAS, that does not require any user intervention during the transformation and analysis phases, thus making the consistency analysis usable by non-expert practitioners. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive system called the Fuel Level Display.

Place, publisher, year, edition, pages
United States: ACM , 2017. Vol. 17, no 4, p. 15-28
Keywords [en]
Requirements Consistency Analysis, Formal Methods, SMT, Z3
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-38940DOI: 10.1145/3183628.3183630ISI: 000424075800002OAI: oai:DiVA.org:mdh-38940DiVA, id: diva2:1205974
Projects
VeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyAvailable from: 2018-05-15 Created: 2018-05-15 Last updated: 2018-07-25Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Filipovikj, PredragRodriguez-Navas, GuillermoSeceleanu, Cristina

Search in DiVA

By author/editor
Filipovikj, PredragRodriguez-Navas, GuillermoSeceleanu, Cristina
By organisation
Embedded Systems
In the same journal
ACM SIGAPP Applied Computing Review
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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