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
A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
ALL4TEC, Laval, France.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-4040-3480
2015 (English)In: Advances in Computers, Cornelsen, 2015, Vol. 98, 89-140 p.Chapter in book (Refereed)
Abstract [en]

Software testing aims at gaining confidence in software products through fault detection, by observing the differences between the behavior of the implementation and the expected behavior described in the specification. Nowadays, testing is the main verification technique used in industry, being a time and resource consuming activity. This has boosted the development of potentially more efficient testing techniques, like model-based testing, where test creation and execution can be automated, using an abstract system model as input. In this chapter, we provide an overview of the state-of-the-art in tool-supported model-based testing that starts from requirements-based models, by presenting and classifying some of the most mature tools available at this moment. Our goal is to get a deeper insight into the state-of-the-art in this area, as well as to form a position with respect to possible needs and gaps in the current tools used by industry and academia, which need to be addressed in order to enhance the applicability of model-based testing techniques. To achieve this, we extend an existing taxonomy with: (i) the test artifact, representing the type of information encoded in the model for the purpose of testing (i.e., functional behavior, extra-functional behavior, or the architectural description), and (ii) the mapping of test cases, which describes ways of using the generated test cases on the actual system under test. To provide further evidence of the inner-workings of different model-based testing tools, we select four representative tools (i.e, ProTest, UPPAAL Cover, MaTeLo, and CompleteTest) that we apply on a simple yet illustrative Coffee/Tea Vending Machine example, to show the differences in modeling notations, test case generation methods, and the produced test-cases. 

Place, publisher, year, edition, pages
Cornelsen, 2015. Vol. 98, 89-140 p.
Keyword [en]
Classification, Formal modeling, Literature review, Model-based testing, Model-checking, Requirements-based design, Survey, Taxonomy, Tool support, Tools for model-based testing
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-29464DOI: 10.1016/bs.adcom.2015.03.003ISI: 000370521900004Scopus ID: 2-s2.0-84945485590ISBN: 9780128021323 (print)OAI: oai:DiVA.org:mdh-29464DiVA: diva2:868901
Available from: 2015-11-12 Created: 2015-11-12 Last updated: 2016-12-27Bibliographically approved
In thesis
1. Model-driven Analysis and Verification of Automotive Embedded Systems
Open this publication in new window or tab >>Model-driven Analysis and Verification of Automotive Embedded Systems
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Modern vehicles are equipped with electrical and electronic systems that implement highly complex functions, such as anti-lock braking, cruise control, etc. To realize and integrate such complex embedded systems, the automotive development process requires an updated methodology that takes into consideration the system’s intricate features and examines both their functional and extra-functional requirements. Early design artifacts like architectural models represent convenient abstractions for reasoning about the system’s structure and functionality. In this context, the EAST-ADL language has been developed as a domain-specific architectural language that targets the automotive industry and is aligned with the AUTOSAR automotive standard. To fully enjoy the benefits of these abstract system descriptions, architectural models need to be integrated into a model-driven development framework that enables also verification by, e.g., model checking and model-based testing. One major drawback in developing such a framework lies in the fact that architectural models, while capturing the system’s structure and inter-component communication, often lack direct means to represent the desired internal behavior of the system in a semantically well-defined way. To overcome this, one needs to provide means of integrating both structural as well as behavioral information, desirably within the same framework backed by formal semantics, in order to enable the model’s formal verification.

In this thesis, we propose a tool-supported integrated formal modeling and verification framework tailored for automotive embedded systems that are originally described in the EAST-ADL architectural language. To achieve this, we first provide formal semantics to the architectural model and its behavior by proposing an equivalent formal description as a network of timed automata. This enables us to analyze the resulting network of timed automata formally by model checking, using both the UPPAAL PORT and UPPAAL SMC model checkers. UPPAAL PORT is providing efficient component-aware verification via the partial order reduction technique, while UPPAAL SMC is extending UPPAAL with statistical model-checking capabilities via probabilistic algorithms. We focus the analysis on functional and timing requirements, but also on the system’s resource usage with respect to different resources specified in the model, such as memory and energy. In an attempt to narrow the gap between the original architectural model and the eventual system implementation, we define an executable semantics of the UPPAAL PORT components that guarantees that the implementation preserves the invariant properties of the model. Assuming a system implementation that conforms to the formal model, we investigate how to provide test cases suitable for the eventual verification of such implementation, by exploiting the model checker’s ability to generate witness traces for reachability verification. Such a witness trace represents a execution of the system from its initial state to the goal state encoded by the reachability property, and becomes our abstract test case. By pairing the automated model-based test case generator with an automatic transformation from the abstract test cases to Python scripts, we enable the execution of the generated Python scripts on the system under test, which ends up in pass/fail testing verdicts. Dependency analysis is a method that is able to identify crucial intra- and inter-component dependencies early in the system’s development life cycle, if applied on architectural models. In this thesis, we also investigate how such dependencies, resulting from applying dependency analysis on EAST-ADL models, can be exploited during formal verification in order to reduce the verified state-spaces during model checking. The framework is supported by the ViTAL tool and its applicability is shown on an automotive industrial prototype, namely a Brake-by-Wire system. 

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2016
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 206
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-32463 (URN)978-91-7485-278-3 (ISBN)
External cooperation:
Public defence
2016-10-07, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2016-08-17 Created: 2016-08-17 Last updated: 2016-09-12Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Marinescu, RalucaSeceleanu, CristinaPettersson, Paul
By organisation
Embedded Systems
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 41 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