Change search
ReferencesLink to record
Permanent link

Direct link
Model-driven Analysis and Verification of Automotive Embedded Systems
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
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: urn:nbn:se:mdh:diva-32463ISBN: 978-91-7485-278-3OAI: oai:DiVA.org:mdh-32463DiVA: diva2:953483
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
List of papers
1. 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 (ScopusID)
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: 2016-08-17Bibliographically approved
2. Analyzing Industrial Architectural Models by Simulation and Model-Checking
Open this publication in new window or tab >>Analyzing Industrial Architectural Models by Simulation and Model-Checking
Show others...
2015 (English)In: Communications in Computer and Information Science, vol. 476, 2015, 2015, 189-205 p.Conference paper (Refereed)
Abstract [en]

The software architecture of any automotive system has to be decided well in advance of production, so it is very desirable to assess its quality in order to obtain quick indications of errors at early design phases. In this paper, we present a constellation of analysis techniques for architectural models described in EAST-ADL. The methods are complementary in terms of covering EAST-ADL model analysis against a rich set of requirements, and in terms of the varying degree of confidence in the provided guarantees. Based on the needs of the current model- driven development in a chosen automotive context, we propose three analysis techniques of EAST-ADL architectural models, in an attempt to tackle some of the exposed design needs: simulation of EAST-ADL functions in Simulink, model-checking EAST-ADL models with timed automata semantics, and statistical model-checking in UPPAAL, applied on an automatically generated network of timed automata. An indus- trial Brake-by-Wire prototype is the case study on which we show the potential of simulating EAST-ADL models in Simulink, model-checking downscale EAST-ADL models, as well statistical model-checking of full model versions, in order to tame verification scalability problems.

National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-26801 (URN)10.1007/978-3-319-17581-2_13 (DOI)000368430500013 ()2-s2.0-84929618771 (ScopusID)978-331917580-5 (ISBN)
Conference
Third International Workshop on Formal Techniques for Safety-Critical Systems FTSCS2014, 6-7 Nov 2014, Luxembourg, Luxemburg
Projects
MBAT - Combined Model-based Analysis and Testing (Artemis/Vinnova)
Available from: 2014-12-03 Created: 2014-12-02 Last updated: 2016-08-17Bibliographically approved
3. Statistical Analysis of Resource Usage of Embedded Systems Modeled in EAST-ADL
Open this publication in new window or tab >>Statistical Analysis of Resource Usage of Embedded Systems Modeled in EAST-ADL
2015 (English)In: IEEE Computer Society Annual Symposium on VLSI (ISVLSI), 2015, 380-385 p.Conference paper (Refereed)
Abstract [en]

The growing complexity of modern automotive embedded systems requires new techniques for model-based design that takes under consideration both software and hardware constraints and enables verification at early stages of development. In this context, EAST-ADL was developed as a domain specific language dedicated to modeling of functional-, software-, and hardware- architecture of automotive embedded systems. This language represents a convenient abstraction when reasoning about the system functionality and supports modeling of relevant extra-functional properties, like timing and resource usage. By providing formal semantics to the EAST-ADL language, as a network of priced timed automata, it becomes possible to reason about feasibility and worst-case resource consumption of the embedded components. In this paper, we show how to analyze such embedded systems modeled in EAST-ADL by using statistical model-checking. We report our experiences from applying this approach to an industrial Brake-by-Wire system.

National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-30439 (URN)10.1109/ISVLSI.2015.103 (DOI)000377094100068 ()2-s2.0-84956968739 (ScopusID)978-1-4799-8718-4 (ISBN)
Conference
IEEE Computer Society Annual Symposium on VLSI ISVLSI, 8-10 Jul 2015, Montpellier, France
Projects
ITS-EASY Post Graduate School for Embedded Software and SystemsVeriSpec - Structured Specification and Automated Verification for Automotive Functional SafetyTOCSYC - Testing of Critical System Characteristics (KKS)
Available from: 2015-12-21 Created: 2015-12-21 Last updated: 2016-08-17Bibliographically approved
4. A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs
Open this publication in new window or tab >>A Research Overview of Tool-Supported Model-based Testing of Requirements-based Designs
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
Keyword
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:nbn:se:mdh:diva-29464 (URN)10.1016/bs.adcom.2015.03.003 (DOI)000370521900004 ()2-s2.0-84945485590 (ScopusID)9780128021323 (ISBN)
Available from: 2015-11-12 Created: 2015-11-12 Last updated: 2016-08-17Bibliographically approved

Open Access in DiVA

fulltext(2001 kB)28 downloads
File information
File name FULLTEXT02.pdfFile size 2001 kBChecksum SHA-512
99e0dcdd8cf298f15a4959ff81e110dadb798ea898906bdcab1cead23d36ceb657902c4ced5b2e554631f63f7a1081a5bdd928aa86e9f0416b103f8748ef38c8
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: 28 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

Total: 357 hits
ReferencesLink to record
Permanent link

Direct link