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
Model-checking and Model-based Testing of Automotive Embedded Systems: Starting from the System Architecture
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
2014 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Nowadays, modern vehicles are equipped with electrical and electronic systems that implement highly complex functions such as anti-lock braking or cruise control. The use of such embedded systems in the automotive domain requires a revised development process that addresses their particular features. In this context, architectural models have been introduced in system development as convenient abstractions of the system’s structure represented as interacting components. To enjoy the full benefits of such abstractions, the architectural models should be complemented by an analysis framework that provides means for formal verification, and ideally also model-based testing, tailored to complex automotive systems. One major difficulty in developing such a framework lies in the fact that architectural models represent the system’s structure as well as inter-component communication, often without the actual description of the behavior. This entails the need to integrate the two “views” (structural and behavioral) in order to integrate them in a formal framework for verification.

In this thesis, we propose an integrated formal modeling and analysis methodology for automotive embedded systems that are originally described in the domain-specific architectural language EAST-ADL. Our analysis methodology relies on formal veri- fication of the original EAST-ADL model by model-checking with UPPAAL PORT for component-based analysis, and UPPAAL SMC for statistical model-checking. To enable this, we first propose a formal description of the EAST-ADL components as networks of timed automata (TA), which are UPPAAL’s modeling language. Since C code implementation is in fact what is deployed on the vehicle, it is highly desirable to narrow the gap between the code and the architectural model, but also to test the implementation for various requirements. To accomplish the former, we define an exe- cutable semantics of the UPPAAL PORT components. To be able to support testing of EAST-ADL based implementations, we take advantage of the model-checker’s ability to generate witness traces during verification of reachability properties. Consequently, we employ UPPAAL PORT to generate such traces that become our abstract test-cases. 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 (our concrete test cases) on the system under test. The entire formal analysis and model-based testing framework is one solution to analyzing EAST-ADL models by model-checking techniques We show the framework’s applicability on an automotive industrial prototype, namely a Brake-by-Wire system. 

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2014.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 188
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-26501ISBN: 978-91-7485-177-9 (print)OAI: oai:DiVA.org:mdh-26501DiVA: diva2:761903
Presentation
2014-12-19, Gamma, Mälardalens högskola, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2014-11-10 Created: 2014-11-09 Last updated: 2014-12-12Bibliographically approved
List of papers
1. A Model-Based Testing Framework for Automotive Embedded Systems
Open this publication in new window or tab >>A Model-Based Testing Framework for Automotive Embedded Systems
Show others...
2014 (English)In: The 40th Euromicro Conference on Software Engineering and Advanced Applications SEAA 2014, Verona, Italy, 2014Conference paper, Published paper (Refereed)
Abstract [en]

Architectural models, such as those described in the EAST-ADL language, represent convenient abstractions to reason about automotive embedded software systems. To enjoy the fully-fledged advantages of reasoning, EAST-ADL models could benefit from a component-aware analysis framework that provides, ideally, both verification and model-based test-case generation capabilities. While different verification techniques have been developed for architectural models, only a few target EAST-ADL. In this paper, we present a methodology for code validation, starting from EAST-ADL artifacts. The methodology relies on: (i) automated model-based test-case generation for functional requirements criteria based on the EAST-ADL model extended with timed automata semantics, and (ii) validation of system implementation by generating Python test scripts based on the abstract test-cases, which represent concrete test-cases that are executable on the system implementation. We apply our methodology to analyze the ABS function implementation of a Brake-by-Wire system prototype.

Place, publisher, year, edition, pages
Verona, Italy: , 2014
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-26419 (URN)10.1109/SEAA.2014.70 (DOI)000358153200006 ()2-s2.0-84916600878 (Scopus ID)
Conference
The 40th Euromicro Conference on Software Engineering and Advanced Applications SEAA 2014, 27-29 Aug 2014, Verona, Italy
Projects
MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova)ITS-EASY Post Graduate School for Embedded Software and Systems
Available from: 2014-11-01 Created: 2014-10-31 Last updated: 2016-06-01Bibliographically approved
2. A Methodology for Formal Analysis and Verification of EAST-ADL Models
Open this publication in new window or tab >>A Methodology for Formal Analysis and Verification of EAST-ADL Models
Show others...
2013 (English)In: Reliability Engineering & System Safety, ISSN 0951-8320, E-ISSN 1879-0836, Vol. 120, no Special Issue, 127-138 p.Article in journal (Refereed) Published
Abstract [en]

The architectural design of embedded software has a direct impact on the final implementation, with respect to performance and other quality attributes. Therefore, guaranteeing that an architectural model meets the specified requirements is beneficial for detecting software flaws early in the development process. In this paper, we present a formal modeling and verification methodology for safety-critical automotive products that are originally described in the domain-specific architectural language East-adl. We propose a model-based approach that integrates the architectural models with component-aware model checking, and describe its tool support called ViTAL. The functional and timing behavior of each function block in the East-adl model, as well as the interactions between function blocks are formally captured and expressed as Timed Automata models, which have precise semantics and can be formally verified with ViTAL. Furthermore, we show how our approach, supported by ViTAL, can be used to formally prove that the East-adl system model fulfills the specified real-time requirements and behavioral constraints. We demonstrate that the approach improves the modeling and verification capability of East-adl and identifies dependencies, as well as potential conflicts between different automotive functions before implementation. The method is substantiated by verifying an automotive braking system model, with respect to particular functional and timing requirements.

Place, publisher, year, edition, pages
Elsevier, 2013
Keyword
EAST-ADL, UPPAAL PORT, Formal Analysis, Model-driven Development, Model transformation
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-21308 (URN)10.1016/j.ress.2013.06.007 (DOI)000324974000016 ()2-s2.0-84885617457 (Scopus ID)
Projects
ATAC - Advanced Test Automation for Complex Software-Intensive System (ITEA2/Vinnova)MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova)
Available from: 2013-09-20 Created: 2013-09-11 Last updated: 2017-12-06Bibliographically approved

Open Access in DiVA

fulltext(1838 kB)536 downloads
File information
File name FULLTEXT02.pdfFile size 1838 kBChecksum SHA-512
0b211ab6769143b458db5b02b5c206ef4f609b852cae957028e56cdad0f419c6d13d88451a1e31f328c97cb78f6fd9874a73517c0572d02daae4b6ed3a52d4f3
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Marinescu, Raluca
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 536 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 916 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