https://www.mdu.se/

mdu.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
Supporting automated containment checking of software behavioural models using model transformations and model checking
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. University of Vienna, Vienna, Austria.
University of Vienna, Vienna, Austria.
University of Vienna, Vienna, Austria.
2019 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, p. 38-71Article in journal (Refereed) Published
Abstract [en]

Models are extensively used in many areas of software engineering to represent the behaviour of software systems at different levels of abstraction. Because of the involvement of different stakeholders in constructing these models and their independent evolution, inconsistencies might occur between the models. It is thus crucial to detect these inconsistencies at early phases of the software development process, and especially as soon as refined models deviate from their abstract counterparts. In this article, we introduce a containment checking approach to verify whether a certain low-level behaviour model, typically created by refining and enhancing a high-level model, still is consistent with the specification provided in its high-level counterpart. We interpret the containment checking problem as a model checking problem, which has not received special treatment in the literature so far. Because the containment checking is based on model checking, it requires both formal consistency constraints and specifications of these models. Unfortunately, creating formal consistency constraints and specifications is currently done manually, and therefore, labour-intensive and error prone. To alleviate this issue, we define and develop a fully automated transformation of behaviour models into formal specifications and properties. The generated formal specifications and properties can directly be used by existing model checkers for detecting any discrepancy between the input models and yield corresponding counterexamples. Moreover, our approach can provide the developers more informative and comprehensive feedback regarding the inconsistency issues, and therefore, help them to efficiently identify and resolve the problems. The evaluation of various scenarios from industrial case studies demonstrates that the proposed approach efficiently translates the behaviour models into formal specifications and properties. 

Place, publisher, year, edition, pages
Elsevier B.V. , 2019. Vol. 174, p. 38-71
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-42630DOI: 10.1016/j.scico.2019.01.005ISI: 000461533200002Scopus ID: 2-s2.0-85060535302OAI: oai:DiVA.org:mdh-42630DiVA, id: diva2:1287386
Available from: 2019-02-11 Created: 2019-02-11 Last updated: 2019-04-04Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

UL Muram, Faiz

Search in DiVA

By author/editor
UL Muram, Faiz
By organisation
Embedded Systems
In the same journal
Science of Computer Programming
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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