Verification of structural and extra-functional properties in component and connector models for embedded and cyber-physical systems

von Wenckstern, Michael; Rumpe, Bernhard; Maoz, Shahar

doi:39173

Verification of structural and extra-functional properties in component and connector models for embedded and cyber-physical systems

von Wenckstern, Michael^RWTH*

2020 & 2022

VerantwortlichkeitsangabeMichael von Wenckstern, RWTH Aachen University

ImpressumDüren : Shaker 2020

Umfang440 Seiten : Illustrationen, Diagramme

ISBN3-8440-7239-X, 978-3-8440-7239-6

ReiheAachener Informatik Berichte, Software Engineering ; 44

Dissertation, RWTH Aachen University, 2019

Druckausgabe: 2020. - Zweitveröffentlicht auf dem Publikationsserver der RWTH Aachen University 2022

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Rumpe, Bernhard (Thesis advisor)^RWTH* ; Maoz, Shahar (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2019-10-31

Online
DOI: 10.18154/RWTH-2020-06045
URL: https://publications.rwth-aachen.de/record/792350/files/792350.pdf
URL: http://digitale-objekte.hbz-nrw.de/storage2/2020/07/09/file_21/8883681.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Cyber-physisches System (Genormte SW) ; Grafische Darstellung (Genormte SW) ; Requirements engineering (Genormte SW) ; Eingebettetes System (Genormte SW) ; Komponente (Genormte SW) ; OCL (Genormte SW) ; Konnektor (Genormte SW) ; AML (Genormte SW) ; Modellgetriebene Entwicklung (Genormte SW)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
The industry area of embedded and cyber-physical systems is one of the largest and it influencesour daily life. The global embedded systems marked was valued at about 160 billion US dollar in2015 and it is getting up to 225 billion US dollar by end of 2021 [Zio17]. Example domains ofembedded and cyber-physical systems are: automotive [DHJ+08], avionics [FLV03], robotics[WICE03], railway [DNCH10], production industry [EWSG94], telecommunication [ZSM11],healthcare [ERA09], defense [BNP+04], and consumer electronics [VOVDLKM00].Model-based engineering, esp. component and connector (C&C) models to describe logicalarchitectures, are one common approach to handle the large complexity of embedded andcyber-physical systems [FR07,MBNJ09,OMG15,EJL+03]. Components encapsulate softwarefeatures; the hierarchical decomposition of components enables formulating logical architecturesin a top-down approach. Connectors in C&C models describe the information exchange via typedports; they model black-box communication between software features.The current development of complex C&C-based embedded systems in industry mostly in-volves the following steps [BMR+17a,DGH+19]: (1) formulating functional and extra-functionalrequirements as text inIBM Rational DOORS; (2) creating a design model of the software architec-ture including its environment interactions inSysML; (3) developing a complete functional/logicalmodel to simulate the embedded system inSimulink; and (4) system implementation based onavailable hardware in C/C++ satisfying all extra-functional properties.This current development process has the following disadvantages [KBFS12,HKK+18,BMR+17a]: (a)SysMLmodels do not follow a formalized approach; i.e., engineers may interpretthese models differently due to missing semantics; (b) the check between the informalSysMLarchitecture design against theSimulinkmodel is done manually, and thus, error-prone and verytime-consuming; (c) refactoring ofSimulinkmodels (e.g., dividing a subsystem) needs manualeffort in updating the design model, and therefore, due to timing constraints this step is oftenskipped resulting in inconsistencies; and (d) most tools do not support a generic approach fordifferent extra-functional property kinds, and thus, extra-functional properties are mostly modeledas comments or stereotypes and consistencies between these properties are checked manually.This thesis aims to improve the software development process of large and complex C&Cmodels for embedded and cyber-physical systems by providing model-based methodologies todevelop, understand, validate and maintain these C&C models. Concrete, this thesis presentsconcepts to support the embedded software engineer with: (i) automatic consistency checks ofC&C models; (ii) automatic verification of logical C&C models against their design decisions;(iii) automatic addition of traceability links between design and implementation models; (iv)finding structural inconsistencies during model evolution; (v) providing a flexible framework todefine different extra-functional property types; (vi) presenting anOCLframework to specify(company-specific) constraints about structural or extra-functional properties for C&C models;and (vii) generation of positive or negative witnesses to explain why a C&C model satisfies orviolates its extra-functional or structural constraints or its design decisions.Prototype implementations of above mentioned concepts and an industrial case study incooperation with Daimler AG show promising results in improving the model-based developmentprocess of embedded and cyber-physical systems in industry.

OpenAccess:
PDF
External link:
Table of contents