mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
ReSA Tool: Structured requirements specification and SAT-based consistency checking
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modelling and Analysis of Embedded Systems)ORCID iD: 0000-0002-5626-0587
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modelling and Analysis of Embedded Systems)ORCID iD: 0000-0003-2870-2680
Volvo Group Trucks Technology, Sweden.
2016 (English)In: ReSA Tool: Structured requirements specification and SAT-based consistency-checking, 2016, 1737-1746 p.Conference paper (Refereed)
Abstract [en]

Most industrial embedded systems requirements are specified in natural language, hence they can sometimes be ambiguous and error-prone. Moreover, employing an early-stage model-based incremental system development using multiple levels of abstraction, for instance via architectural languages such as EAST-ADL, calls for different granularity requirements specifications described with abstraction-specific concepts that reflect the respective abstraction level effectively. In this paper, we propose a toolchain for structured requirements specification in the ReSA language, which scales to multiple EAST-ADL levels of abstraction. Furthermore, we introduce a consistency function that is seamlessly integrated into the specification toolchain, for the automatic analysis of requirements logical consistency prior to their temporal logic formalization for full formal verification. The consistency check subsumes two parts: (i) transforming ReSA requirements specification into boolean expressions, and (ii) checking the consistency of the resulting boolean expressions by solving the satisfiability of their conjunction with the Z3 SMT solver. For validation, we apply the ReSA toolchain on an industrial vehicle speed control system, namely the Adjustable Speed Limiter.

Place, publisher, year, edition, pages
2016. 1737-1746 p.
Series
2016 Federated Conference on Computer Science and Information Systems (FedCSIS
Keyword [en]
requirements specification, consistency checking, formal methods, embedded systems, automotive systems, software tool
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-34005DOI: 10.15439/2016F404ISI: 000392436600246ScopusID: 2-s2.0-85007240246ISBN: 978-8-3608-1090-3 (print)OAI: oai:DiVA.org:mdh-34005DiVA: diva2:1050648
Conference
2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016; Gdansk; Poland; 11 September 2016 through 14 September 2016
Projects
VeriSpec
Funder
VINNOVA, 16335
Available from: 2016-11-29 Created: 2016-11-29 Last updated: 2017-02-23Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Mahmud, NesredinSeceleanu, Cristina
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 10 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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