hh.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
Modal Transition System Encoding of Featured Transition Systems
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).ORCID iD: 0000-0002-4776-883X
Technische Universität Darmstadt, Darmstadt, Germany.
Technische Universität Darmstadt, Darmstadt, Germany.
Technische Universität Darmstadt, Darmstadt, Germany.
Show others and affiliations
2019 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 106, p. 1-28Article in journal (Refereed) Published
Abstract [en]

Featured transition systems (FTSs) and modal transition systems (MTSs) are two of the most prominent and well-studied formalisms for modeling and analyzing behavioral variability as apparent in software product line engineering. On one hand, it is well-known that for finite behavior FTSs are strictly more expressive than MTSs, essentially due to the inability of MTSs to express logically constrained behavioral variability such as persistently exclusive behaviors. On the other hand, MTSs enjoy many desirable formal properties such as compositionality of semantic refinement and parallel composition. In order to finally consolidate the two formalisms for variability modeling, we establish a rigorous connection between FTSs and MTSs by means of an encoding of one FTS into an equivalent set of multiple MTSs. To this end, we split the structure of an FTS into several MTSs whenever it is necessary to denote exclusive choices that are not expressible in a single MTS. Moreover, extra care is taken when dealing with infinite behaviour: loops may have to be unrolled to accumulate FTS path constraints when encoding them into MTSs. We prove our encoding to be semanticpreserving (i.e., the resulting set of MTSs induces, up to bisimulation, the same set of derivable variants as their FTS counterpart) and to commute with modal refinement. We further give an algorithm to calculate a concise representation of a given FTS as a minimal set of MTSs. Finally, we present experimental results gained from applying a tool implementation of our approach to a collection of case studies.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2019. Vol. 106, p. 1-28
Keywords [en]
Featured Transition Systems, Modal Transition Systems, Expressiveness Power, Product Lines, Modeling
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:hh:diva-38941DOI: 10.1016/j.jlamp.2019.03.003ISI: 000474505200001Scopus ID: 2-s2.0-85054040481OAI: oai:DiVA.org:hh-38941DiVA, id: diva2:1289495
Projects
AUTO-CAAS
Funder
Knowledge Foundation, 20140312Swedish Research Council, 621-2014-5057ELLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications
Note

Funding: The work of Mahsa Varshosaz and Mohammad Reza Mousavi has been partially supported by grants from the Swedish Knowledge Foundation (Stiftelsen för Kunskaps- och Kompetensutveckling) in the context of the AUTO-CAAS HoGproject (number: 20140312), Swedish Research Council (Vetenskapsrådet) award number: 621-2014-5057 (Effective Model-Based Testing of Concurrent Systems), and the ELLIIT Strategic Research Environment. The work of Lars Luthmann, Paul Mohr and Malte Lochau has been supported by the German Research Foundation (DFG) in the Priority Programme SPP 1593: Design For Future – Managed Software Evolution (LO 2198/2-1).

Available from: 2019-02-18 Created: 2019-02-18 Last updated: 2021-05-06Bibliographically approved
In thesis
1. Modeling and Model-Based Testing of Software Product Lines
Open this publication in new window or tab >>Modeling and Model-Based Testing of Software Product Lines
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Software product line (SPL) engineering has become common practice for mass production and customization of variability intensive systems. A software product line comprises a family of software systems which share a managed core set of artifacts and also have a set of well-defined variabilities. The main idea in SPL engineering is to enable systematic reuse in different phases of software development to reduce cost and time to release.

Model-Based Testing (MBT) is a technique that is widely used for quality assurance of software systems. In MBT, an abstract model, which captures the desired behavior of the system, is used to generate test cases. The test cases are executed against a real implementation of the system and the conformance between the implementation and the specification is checked by comparing the observed outputs with the ones prescribed by the model.

Software product lines have been applied in a number of domains with mission critical systems. MBT is one of the techniques that has been used for analysis of such systems. As the number of products can be potentially large in an SPL, using conventional approaches for MBT of the products of an SPL individually can be very costly and time consuming. To tackle this problem, several approaches have been proposed in order to enable systematic reuse in different phases of the MBT process.

An efficient modeling technique is the first step towards an efficient MBT technique for SPLs. So far, several formalisms have been proposed for modeling SPLs. In this thesis, we conduct a study on such modeling techniques, focusing on four fundamental formalisms, namely featured transition systems, modal transition systems, product line calculus of communicating systems, and 1- selecting modal transition systems. We compare the expressive power and the succinctness of these formalisms.

Furthermore, we investigate adapting existing MBT methods for efficient testing of SPLs. As a part of this line of our research, we adapt the test case generation algorithm of one of the well-known black-box testing approaches, namely, Harmonized State Identification (HSI) method by exploiting the idea of delta-oriented programming. We apply the adapted test case generation algorithm to a case study taken from industry and the results show up to 50 percent reduction of time in test case generation by using the delta-oriented HSI method.

In line with our research on investigating existing MBT techniques, we compare the relative efficiency and effectiveness of the test case generation algorithms of the well-known Input-Output Conformance (ioco) testing approach and the complete ioco which is another testing technique used for input output transition systems that guarantees fault coverage. The comparison is done using three case studies taken from the automotive and railway domains. The obtained results show that complete ioco is more efficient in detecting deep faults (i.e., the faults reached through longer traces) in large state spaces while ioco is more efficient in detecting shallow faults (i.e., the faults reached through shorter traces) in small state spaces.

Moreover, we conduct a survey on sampling techniques, which have been proposed as a solution for handling the large number of products in analysis. In general, in product sampling a subset of products that collectively cover the behavior of the product line are selected. Performing tests on well selected sample set can reveal most of the faults in all products. We provide a classification for a catalog of studies on product sampling for software product lines. Additionally, we present a number of insights on the studied work as well as gaps for the future research.

Place, publisher, year, edition, pages
Halmstad: Halmstad University Press, 2019
Series
Halmstad University Dissertations ; 54
National Category
Computer Systems
Identifiers
urn:nbn:se:hh:diva-38921 (URN)978-91-88749-16-1 (ISBN)978-91-88749-17-8 (ISBN)
Public defence
2019-02-27, HAV, H22, Kristian IV:s väg 3, Halmstad, 13:00 (English)
Opponent
Supervisors
Available from: 2019-02-18 Created: 2019-02-15 Last updated: 2021-05-06Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Varshosaz, Mahsa

Search in DiVA

By author/editor
Varshosaz, Mahsa
By organisation
Centre for Research on Embedded Systems (CERES)
In the same journal
The Journal of logical and algebraic methods in programming
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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