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

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