@inproceedings{, author = {Blaschke, Konstantin Rupert}, title = {Automated Model Quality Estimation and Change Impact Analysis on Model Histories}, booktitle = {IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion ’24)}, publisher = {To appear}, pages = {3}, year = {2024}, month = apr, owner = {Konstantin Rupert Blaschke}, abstract = {The development of Cyber-Physical Systems combines hardware with software in complex applications. To mitigate the complexity, collaborating system engineers rely on model-based approaches in systems engineering. Updates and function enhancements lead to frequent changing constraints and objectives. These changes increase the need to rework and extend model artifacts of the system. This can cause quality degradation over time due to errors, knowledge disparities or a lack of guidelines. To enable efficient collaboration and reduce maintenance costs in model-based systems engineering, industry needs a cost-efficient, scalable approach to monitor, and control model quality. The work outlines a doctoral thesis investigating the potential of automated data-driven quality assessment strategies using model artifact history and model changes. We will extract metrics and model changes to establish a quality feedback loop for system engineers. We aim to leverage the results of manual model quality assessments to incorporate domain-specific expert knowledge into the automated strategy. The main goal is to lower the effort of model quality assessments and provide practitioners with foresight on quality development and estimate task effort to improve model artifact quality.}, isbn = {979-8-4007-0502-1/24/04}, doi = {10.1145/3639478.3639809}, keywords = {Model-based Systems Engineering, Model Quality, Model Metrics, Quality Assessment, Model Review, Change-Impact Analysis, MbSE, AutoFOCUS3}, } @inproceedings{, author = {Bergemann, Sebastian}, title = {Towards Confidentiality in Multi-Model Inconsistency Detection for Systems Engineering}, booktitle = {2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)}, publisher = {IEEE}, year = {2023}, month = oct, abstract = {Multi-model consistency management is used to keep models with overlapping information consistent during model-based systems engineering. Checking consistency between different models requires model data to be exchanged in some form between the modeling tools. However, in industrial practice such models can contain confidential data that must not be revealed to unauthorized parties, e.g., other departments or external companies. Therefore, it is a critical problem when the consistency management tool does not respect this. We found that none of the current multi-model consistency management approaches in literature consider this problem and provide suitable protections to prevent possible confidential data theft caused by consistency checking. Hence, we propose an approach and implementation for confidentiality preservation in multi-model inconsistency detection that does not reveal confidential model data to unauthorized parties and increases the trustworthiness of the consistency checking process regarding data confidentiality. In this paper we explain the problem and propose our basic solution idea and evaluation plan for our doctoral research.}, doi = {10.1109/MODELS-C59198.2023.00039}, keywords = {consistency management, multi-model inconsistency detection, confidentiality, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Terzimehić, Tarik and Groh, Eddie and Zoitl, Alois}, title = {Composing Services with SMT-Based Deployment Optimization and Service Merging Heuristic}, booktitle = {28th International Conference on Emerging Technologies and Factory Automation (ETFA)}, publisher = {IEEE}, year = {2023}, month = sep, timestamp = 2023.09.13, location = {Sinaia, Romania}, abstract = {The complexity of Industry 4.0 systems makes it challenging to manually synthesize and optimize architecture level decisions, such as service deployment and composition. To address this challenge, we propose an approach that utilizes a satisfiability modulo theories (SMT) solver to (semi-)automate service deployment and composition synthesis. Thereby, we conceptualize, formalize, and implement the complete workflow from input service workflows to valid and optimized service deployments and compositions. We demonstrate the practical application of our approach in an Industry 4.0 scenario, specifically the flexible production of new products. We evaluate the effectiveness of the proposed approach by investigating its benefits in terms of engineering effort, complexity of the resulting IEC 61499-based applications, and improvement of communication coupling quality attribute (QA).}, doi = {10.1109/ETFA54631.2023.10275652}, keywords = {Industry 4.0, IEC 61499, deployment synthesis, service composition, optimization, SMT, Design-Space Exploration, DSE, Model-based Systems engineering, MbSE}, } @misc{, author = {Sorokin, Lev and Munaro, Tiziano and Damir, Safin and Liao, Brian Hsuan-Cheng and Molin, Adam}, title = {{OpenSBT}: A Modular Framework for Search-based Testing of Automated Driving Systems}, year = {2023}, month = jun, timestamp = 2023.06.17, abstract = {Search-based software testing (SBT) is an effective and efficient approach for testing automated driving systems (ADS). However, testing pipelines for ADS testing are particularly challenging as they involve integrating complex driving simulation platforms and establishing communication protocols and APIs with the desired search algorithm. This complexity prevents a wide adoption of SBT and thorough empirical comparative experiments with different simulators and search approaches. We present OpenSBT, an open-source, modular and extensible framework to facilitate the SBT of ADS. With OpenSBT, it is possible to integrate simulators with an embedded system under test, search algorithms and fitness functions for testing. We describe the architecture and show the usage of our framework by applying different search algorithms for testing Automated Emergency Braking Systems in CARLA as well in the high-fidelity Prescan simulator in collaboration with our industrial partner DENSO. OpenSBT is available at this https URL.}, howpublished = {arXiv:2306.10296 [cs.SE]}, doi = {10.48550/arXiv.2306.10296}, keywords = {Search-based software testing, metaheuristics,scenario-based testing, autonomous driving, automated driving, MbSE, Model-based Systems Engineering}, } @article{, author = {Dantas, Yuri Gil and Munaro, Tiziano and C{\^{a}}rlan, Carmen and Nigam, Vivek and Barner, Simon and Fan, Shiqing and Pretschner, Alexander and Sch{\"{o}}pp, Ulrich and Tverdyshev, Sergey}, title = {A Toolchain for Synthesizing and Validating Safety Architectures}, publisher = {Springer}, journal = {SN Computer Science}, volume = {4}, number = {4}, pages = {335}, year = {2023}, month = apr, timestamp = 2023.04.15, abstract = {Autonomous vehicles handle complicated tasks that may lead to harm when performed incorrectly. These harms, in particular when caused by system faults, may be avoided by the deployment of safety architectural patterns, such as the Heterogeneous Duplex pattern. Our goal is to provide safety engineers with computer-aided support for synthesizing architectures with safety architecture patterns. To this end, we build on our previous work in which we proposed a model-based system engineering plugin to enable the model-driven approach using safety architecture patterns. This article proposes a toolchain for synthesizing the structure and switching logic of safety architectures, as well as for validating them through simulation-based fault-injection. We validate our toolchain using an industrial use-case for autonomous driving systems, namely, a Highway Pilot system.}, issn = {2661-8907}, doi = {10.1007/s42979-023-01712-5}, keywords = {Model-based systems engineering, Toolchain, Safety architecture patterns, Reconfiguration, Simulation, MbSE, AutoFOCUS3, DSE}, } @misc{, author = {H{\"{o}}lzl, Florian and Barner, Simon}, title = {Implementing a Model-based Engineering Tool as Web Application}, year = {2023}, month = mar, timestamp = 2023.03.01, abstract = {This paper reports on a study of transferring a desktop-based model-based engineering tool to a web application. The study has been conducted in the WEBMODEL project where the well-established technology stack around the Eclipse platform and the Eclipse Modeling Framework was lifted into a cloud-based environment. As results, a modeling language independent tooling kernel for web-based modeling tools and a minimal prototypical web-based implementation of the AutoFOCUS 3 model-based engineering tool are presented. Furthermore, the report documents experiences and implementation advises gained during the implementation.}, howpublished = {arXiv:2302.14091 [cs.SE]}, doi = {10.48550/arXiv.2302.14091}, keywords = {Model-based Systems Engineering, MbSE, Tooling, Web Technology, AutoFOCUS3; AF3}, } @inproceedings{, author = {Terzimehić, Tarik and Barner, Simon and Dantas, Yuri Gil and Sch{\"{o}}pp, Ulrich and Nigam, Vivek and Ke, Pei}, title = {Safety-Aware Deployment Synthesis and Trade-Off Analysis of Apollo Autonomous Driving Platform}, booktitle = {9th International Workshop on Automotive System/Software Architectures ({WASA}) co-located with {ICSA} 2023}, publisher = {IEEE}, year = {2023}, month = mar, abstract = {The adoption of autonomous cars requires operational critical functions even in the event of HW faults and/or SW defects, and protection of safety-critical functions against security threats. Defining appropriate safe and secure architectures is challenging and costly. In previous work, we have proposed tools to automate the recommendation of safety and security patterns for safety-critical systems. However, safety and security measures may (negatively) influence system performance, besides introducing additional development effort. We present a design space exploration approach, a model-based engineering workflow and tool prototype for automated guidance on trade-off decisions when applying safety and security patterns on a given (unsafe) baseline architecture. Based on models that abstract the vehicle’s functionality and its software and hardware components, as well as an engine for the automated pattern recommendation, we investigate the optimization of HW/SW deployments, and provide a trade-off analysis for different architecture candidates. We implemented our approach in an open-source tool and evaluate it with a model of the Apollo autonomous driving platform.}, doi = {10.1109/ICSA-C57050.2023.00070}, keywords = {Autonomous vehicles, Apollo, model-driven development, system architecture, safety, model-based systems engineering, MbSE, design-space exploration, DSE, AutoFOCUS3, AF3}, } @inproceedings{icissp23_1, author = {Dantas, Yuri Gil and Nigam, Vivek and Sch{\"{o}}pp, Ulrich and Barner, Simon and Ke, Pei}, title = {Automating Vehicle SOA Threat Analysis using a Model-Based Methodology}, booktitle = {Proceedings of the 9th International Conference on Information Systems Security and Privacy (ICISSP)}, publisher = {SciTePress}, pages = {180-191}, year = {2023}, month = feb, abstract = {This article proposes automated methods for threat analysis using a model-based engineering methodology that provides precise guarantees with respect to safety goals. This is accomplished by proposing an intruder model for automotive SOA which together with the system architecture and the loss scenarios identified by safety analysis are used as input for computing assets, impact rating, damage/threat scenarios, and attack paths. To validate the proposed methodology, we developed a faithful model of the autonomous driving functions of the Apollo framework, a widely used open source autonomous driving stack. The proposed machinery automatically enumerates several attack paths on Apollo, including attack paths not reported in the literature.}, isbn = {978-989-758-624-8}, issn = {2184-4356}, doi = {10.5220/0011786400003405}, keywords = {automotive, threat analysis, service-oriented architectures, Apollo, automation, safe and secure-by-design, MbSE, Model-based Systems Engineering, AutoFOCUS3, AF3}, } @article{, author = {Petrovska, Ana and Kugele, Stefan and Hutzelmann, Thomas and Beffart, Theo and Bergemann, Sebastian and Pretschner, Alexander}, title = {Defining adaptivity and logical architecture for engineering (smart) self-adaptive cyber–physical systems}, publisher = {Elsevier}, journal = {Information and Software Technology}, volume = {147}, year = {2022}, month = jul, abstract = {Context: Modern cyber–physical systems (CPSs) are embedded in the physical world and intrinsically operate in a continuously changing and uncertain environment or operational context. To meet their business goals and preserve or even improve specific adaptation goals, besides the variety of run-time uncertainties and changes to which the CPSs are exposed—the systems need to self-adapt. Objective: The current literature in this domain still lacks a precise definition of what self-adaptive systems are and how they differ from those considered non-adaptive. Therefore, in order to answer how to engineer self-adaptive CPSs or self-adaptive systems in general, we first need to answer what is adaptivity, correspondingly self-adaptive systems. Method: In this paper, we first formally define the notion of adaptivity. Second, within the frame of the formal definitions, we propose a logical architecture for engineering decentralised self-adaptive CPSs that operate in dynamic, uncertain, and partially observable operational contexts. This logical architecture provides a structure and serves as a foundation for the implementation of a class of self-adaptive CPSs. Results: First, our results show that in order to answer if a system is adaptive, the right framing is necessary: the system’s adaptation goals, its context, and the time period in which the system is adaptive. Second, we discuss the benefits of our architecture by comparing it with the MAPE-K conceptual model. Conclusion: Commonly accepted definitions of adaptivity and self-adaptive systems are necessary for work in this domain to be compared and discussed since the same terms are often used with different semantics. Furthermore, in modern self-adaptive CPSs, which operate in dynamic and uncertain contexts, it is insufficient if the adaptation logic is specified during the system’s design, but instead, the adaptation logic itself needs to adapt and “learn” during run-time.}, issn = {0950-5849}, doi = {10.1016/j.infsof.2022.106866}, keywords = {Adaptivity, Quality function, Knowledge, Logical architecture, Self-adaptive cyber–physical systems, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Bergemann, Sebastian}, title = {Challenges in Multi-View Model Consistency Management for Systems Engineering}, booktitle = {Modellierung 2022 Satellite Events}, publisher = {Gesellschaft f{\"{u}}r Informatik e.V.}, pages = {77-89}, year = {2022}, month = jun, abstract = {A way to handle the complexity of cyber-physical systems is model-based systems engineering (MBSE) with multiple viewpoints. These viewpoints satisfy different concerns, but they likely have information dependencies and overlaps among each other. Inconsistencies can be introduced whenever there are changes in only some of the views without consistent synchronization in other dependent views. In this paper, we motivate why consistency management is important in multi-view MBSE and define requirements for it. By analyzing the State of the Art, we identify limitations in (multi-view) consistency management approaches, especially for inconsistency detection. Besides general performance issues, we notice primarily that most approaches are limited to or at least tested on only very specific views and tools with homogeneous models and few specific predefined consistency rules. Furthermore, in most approaches we cannot find solutions regarding subsequent updates of consistency rules by the user, allowance of tolerating inconsistency, and handling confidentiality. These literature gaps pose open research challenges for making multi-view consistency management more applicable in the industry.}, doi = {10.18420/modellierung2022ws-009}, keywords = {Model-based Systems Engineering, MbSE, SpesML, Consistency}, url = {https://dl.gi.de/handle/20.500.12116/38805}, } @inproceedings{, author = {Munaro, Tiziano and Muntean, Irina}, title = {Early Assessment of System-Level Safety Mechanisms through Co-Simulation-based Fault Injection}, booktitle = {2022 IEEE Intelligent Vehicles Symposium (IV)}, publisher = {IEEE}, pages = {1703-1708}, year = {2022}, month = jun, abstract = {Depending on the autonomy level, safety assessment leads to different functional safety requirements for advanced driver-assistance systems and autonomous driving functions. To provide the necessary guarantees, technical safety requirements are derived that support the safety case by means of appropriate system architectures. These build on safety mechanisms: Technical solutions responsible for maintaining the intended functionality (fail-operational) or transition to a safe state in the presence of hardware and software faults (fail-safe). As the choice and implementation of such safety mechanisms are critical decisions with a high impact on the overall architecture, their early validation is crucial for an efficient engineering process. However, analytical safety analysis techniques applied to date support only coarse time models and do not provide explicit guidance for considering systemic real-time properties of closed-loop systems. Therefore, we propose a simulation-based fault injection framework to identify problematic emerging temporal behaviors such as instability. In contrast to existing solutions, we leverage the Functional Mock-up Interface (FMI) standard for black-box co-simulation to overcome intellectual property concerns in distributed automotive supply chains and to account for heterogeneous tool landscapes. By considering the allocation of software units to processing elements as well as the communication infrastructure, our contribution allows for the injection and propagation of faults affecting a vehicle's software and its electrical/electronic (E/E) architecture, which is crucial for the assessment of safety mechanisms. Experimental results obtained by applying the approach to an industry-oriented use case indicate its validity and low overhead.}, doi = {10.1109/IV51971.2022.9827327}, keywords = {Model-based Systems Engineering, MbSE, Co-Simulation, Safety Architecture Patterns, ISO 26262}, } @inproceedings{, author = {Terzimehić, Tarik}, title = {Architecture Synthesis for Optimized and Flexible Production}, booktitle = {2022 IEEE/ACM 44th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)}, publisher = {IEEE}, journal = {2022 IEEE/ACM 44th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)}, year = {2022}, month = may, abstract = {The fourth industrial revolution (Industry 4.0) anticipates frequent synthesis and optimization of different architectural design decisions (ADDs) – such as deployment of software components to hardware components, service composition, production planning, and topology (plant layout) synthesis. The frequent manual search for valid and optimal architectural designs is a time- and cognition-consuming task for an engineer. This asks for automating the process of deriving different ADDs. Although automating different ADDs is intensely investigated in other domains, the current research works 1) require higher engineering effort for specifying architecture optimization problems; 2) conduct (only) sequential ADDs, leading to lower solution quality (i.e., sub-optimal production); 3) neglect reconfigurability and reliability of architectures, and, thereby, offer no solution for production downtime; 4) neglect event-based execution semantics while considering timing-related issues. Therefore, I propose a Satisfiability Modulo Theories (SMT)-based framework for joint synthesis and optimization of multi-dimensional ADDs using industrial automation domain models (e.g., plant topology, product recipes, stations capabilities, etc.). This research should bring the following benefits for the practitioners and researchers: 1) reduction of engineering effort for conducting different ADDs; 2) improvement of different quality attributes (e.g., production performance, reconfigurability, reliability, etc.); 3) guideline/support for a practitioner in choosing ADDs workflow to improve given quality attributes.}, doi = {10.1109/ICSE-Companion55297.2022.9793810}, keywords = {architecture synthesis, optimization, design space exploration, Industry 4.0, deployment, service composition, model-based systems engineering, MbSE}, } @inproceedings{, author = {Storath, Cara and Zhang, Zelun Tony and Liu, Yuanting and Hu{\ss}mann, Heinrich}, title = {Building Trust by Supporting Situation Awareness: Exploring Pilots' Design Requirements for Decision Support Tools}, booktitle = {CHI TRAIT '22: Workshop on Trust and Reliance in Human-AI Teams at CHI 2022}, year = {2022}, month = apr, location = {New Orleans, LA}, abstract = {Supporting pilots with a decision support tool (DST) during high-workload scenarios is a promising and potentially very helpful application for AI in aviation. Nevertheless, design requirements and opportunities for trustworthy DSTs within the aviation domain have not been explored much in the scientific literature. To address this gap, we explore the decision-making process of pilots with respect to user requirements for the use case of diversions. We do so via two prototypes, each representing a role the AI could have in a DST: A) Unobtrusively hinting at data points the pilot should be aware of. B) Actively suggesting and ranking diversion options based on criteria the pilot has previously defined. Our work-in-progress feedback study reveals four preliminary main findings: 1) Pilots demand guaranteed trustworthiness of such a system and refuse trust calibration in the moment of emergency. 2) We may need to look beyond trust calibration for isolated decision points and rather design for the process leading to the decision. 3) An unobtrusive, augmenting AI seems to be preferred over an AI proposing and ranking diversion options at decision time. 4) Shifting the design goal toward supporting situation awareness rather than the decision itself may be a promising approach to increase trust and reliance.}, type = {Workshop}, keywords = {human-AI interaction, decision support tools, decision support systems, human-AI teaming, aviation}, url = {https://www.researchgate.net/publication/360166947_Building_Trust_by_Supporting_Situation_Awareness_Exploring_Pilots'_Design_Requirements_for_Decision_Support_Tools}, } @inproceedings{, author = {Dantas, Yuri Gil and Munaro, Tiziano and C{\^{a}}rlan, Carmen and Nigam, Vivek and Barner, Simon and Fan, Shiqing and Pretschner, Alexander and Sch{\"{o}}pp, Ulrich and Tverdyshev, Sergey}, title = {A Model-based System Engineering Plugin for Safety Architecture Pattern Synthesis}, booktitle = {Proceeding of the 10th International Conference on Model-Driven Engineering and Software Development (MODELSWARD)}, publisher = {SCITEPRESS}, pages = {36--47}, year = {2022}, month = feb, abstract = {Safety architecture patterns are abstract representations to address faults in the system architecture. In the current state of practice, the decision of which safety architecture pattern to deploy and where in the system architecture is carried out manually by a safety expert. This decision may be time consuming or even lead to human errors. This paper presents Safety Pattern Synthesis, a tool for automating the recommendation of safety architecture patterns during the design of safety-critical systems: 1) Safety Pattern Synthesis recommends patterns to address faults in the system architecture (possibly resulting in more than one architectural solution), 2) the user selects the system architecture with patterns based on, e.g., the criteria provided by Safety Pattern Synthesis, and 3) Safety Pattern Synthesis provides certain requirements that shall be considered in the overall safety engineering process. The proposed tool has been implemented as a plugin in the model-based system engineering tool called AutoFOCUS3. Safety Pattern Synthesis is implemented in Java while using a logic-programming engine as a backend to reason about the safety of the system architecture. This paper provides implementation details about Safety Pattern Synthesis and its applicability in an industrial case study taken from the automotive domain.}, isbn = {978-989-758-550-0}, doi = {10.5220/0010831700003119}, keywords = {Model-based Systems Engineering, MbSE, Safety Architecture Patterns, Automation, Tooling, DSE}, } @inproceedings{, author = {Mirzaei, Elham and C{\^{a}}rlan, Carmen and Thomas, Carsten and Gallina, Barbara}, title = {Design-time Specification of Dynamic Modular Safety Cases in Support of Run-Time Safety Assessment}, booktitle = {Proceedings of the Thirtieth Safety-Critical Systems Symposium}, publisher = {SCSC}, volume = {170}, year = {2022}, month = feb, abstract = {Open Adaptive Complex Systems – such as road vehicle platoons or fleets of cooperative robots – may use dynamic reconfiguration to adapt to system or environment changes. One approach enabling this feature is Service-oriented Reconfiguration, where new configurations are created by composing the available services in an unconstrained manner. Due to the high number of possible service compositions, not all configurations can be pre-assured at design-time. Despite recent progress, there is no satisfactory approach for specifying safety cases in support of their re-evaluation at run-time, after system reconfiguration. To this end, in previous work, we introduced Dynamic Modular Safety Cases (DMSC). A DMSC is a modular safety case, which can be dynamically re-constructed and re-assessed given service reconfiguration. In continuation of the previous work, in this paper we provide guidelines for specifying safety cases at design-time, whose modular structure mirrors the system service decomposition, to enable their re-construction and re-evaluation at run-time in the event of a system reconfiguration. Aiming to support the specification of DMSC, we extend FASTEN, an engineering tool for the design and verification of safety-critical systems. We exemplify the specification of DMSCs in FASTEN for an illustrative example from the smart factory domain.}, isbn = {9798778289932}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://scsc.uk/rp170.3:1}, } @inproceedings{, author = {Terzimehić, Tarik and Dorofeev, Kirill and Voss, Sebastian}, title = {Exploring Architectural Design Decisions in Industry 4.0: A Literature Review and Taxonomy}, booktitle = {Software Engineering 2022 - Fachtagung des GI-Fachbereichs Softwaretechnik}, publisher = {Gesellschaft f{\"{u}}r Informatik (GI)}, journal = {Software Engineering 2022 - Fachtagung des GI-Fachbereichs Softwaretechnik}, year = {2022}, month = feb, abstract = {Paper accepted in the Foundation Track of ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2021. Architectural design decisions, such as service deployment and composition, plant layout synthesis, or production planning, are an indispensable and overarching part of an industrial manufacturing system design. In the fourth industrial revolution (Industry 4.0), frequent production changes trigger their synthesis, and preferably optimization. Yet, knowledge on architecture synthesis and optimization has been scattered around other domains, such as generic software engineering. We take a step towards synthesizing current knowledge on architectural design decisions in Industry 4.0. We developed a taxonomy describing architectural models, design decisions, and optimization possibilities. The developed taxonomy serves as a guideline for comparing different possibilities (e.g., application of different optimization algorithms) and selecting appropriate ones for a given context. Furthermore, we reviewed and mapped 30 relevant research works to the taxonomy, identifying research trends and gaps. We discuss interesting, and yet uncovered topics that emerged from our review.}, isbn = {978-3-88579-714-2}, doi = {10.18420/se2022-ws-030}, keywords = {architecture synthesis, optimization, taxonomy, design space exploration, MbSE, model-based systems engineering, Industry 4.0}, } @inproceedings{, author = {Terzimehić, Tarik and Dorofeev, Kirill and Voss, Sebastian}, title = {Exploring Architectural Design Decisions in Industry 4.0: A Literature Review and Taxonomy}, booktitle = {ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, publisher = {IEEE}, journal = {ACM/IEEE 24th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, year = {2021}, month = oct, abstract = {Architectural design decisions, such as service deployment and composition, plant layout synthesis, or production planning, are an indispensable and overarching part of an industrial manufacturing system design. In the fourth industrial revolution (Industry 4.0), frequent production changes trigger their synthesis, and preferably optimization. Yet, knowledge on architecture synthesis and optimization has been scattered around other domains, such as generic software engineering. We take a step towards synthesizing current knowledge on architectural design decisions in Industry 4.0. We developed a taxonomy describing architectural models, design decisions, and optimization possibilities. The developed taxonomy serves as a guideline for comparing different possibilities (e.g., application of different optimization algorithms) and selecting appropriate ones for a given context. Furthermore, we reviewed and mapped 30 relevant research works to the taxonomy, identifying research trends and gaps. We discuss interesting, and yet uncovered topics that emerged from our review.}, doi = {10.1109/MODELS50736.2021.00026}, keywords = {architecture synthesis, optimization, taxonomy, design-space exploration, DSE, model-based systems engineering, MbSE, Industry 4.0}, } @inproceedings{, author = {Dorofeev, Kirill and Bergemann, Sebastian and Terzimehić, Tarik and Grothoff, Julian and Thies, Michael and Zoitl, Alois}, title = {Generation of the Orchestrator Code for Skill-Based Automation Systems}, booktitle = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, publisher = {IEEE}, journal = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, year = {2021}, month = sep, abstract = {Engineering distributed control systems is a complex task, where the complexity and, thus, costs of the software development are growing rapidly. To keep the software complexity at an acceptable level and save time for development and subsequent maintenance, new solutions are sorely needed. In this paper, we investigate the advantages of using skills - universal control device interfaces - for generating complex logic in distributed control environments. By enriching a skill interface with the information about the dynamic behavior of a component under control, we compose the functionalities of individual control devices. The logic, required for such composition, is automatically derived from the interface description and the production plan, identifying the required skill sequence. The evaluation, executed using two industrial demonstrators, shows that the approach successfully handles different behavioral models and is capable of generating fault-tolerant orchestrators, including error handling scenarios. Overall, for developing a complex logic in a distributed skill-based automation system, the proposed approach shows significant savings in development time allowing to automate the skill composition task.}, isbn = {978-1-7281-2989-1}, doi = {10.1109/ETFA45728.2021.9613728}, keywords = {Industry 4.0, skills, service-oriented architecture, IEC 61499, service composition, orchestration, PLC code generation, BaSys, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Zhang, Zelun Tony and Liu, Yuanting and Hu{\ss}mann, Heinrich}, title = {Pilot Attitudes Toward AI in the Cockpit: Implications for Design}, booktitle = {2021 IEEE 2nd International Conference on Human-Machine Systems (ICHMS)}, publisher = {IEEE}, year = {2021}, month = sep, location = {Magdeburg, Germany}, abstract = {As the aviation industry is actively working on adopting AI for air traffic, stakeholders agree on the need for a human-centered approach. However, automation design is often driven by user-centered intentions, while the development is actually technology-centered. This can be attributed to a discrepancy between the system designers’ perspective and complexities in real-world use. The same can be currently observed with AI applications where most design efforts focus on the interface between humans and AI, while the overall system design is built on preconceived assumptions. To understand potential usability issues of AI-driven cockpit assistant systems from the users’ perspective, we conducted interviews with four experienced pilots. While our participants did discuss interface issues, they were much more concerned about how autonomous systems could be a burden if the operational complexity exceeds their capabilities. Besides commonly addressed human-AI interface issues, our results thus point to the need for more consideration of operational complexities on a system-design level.}, doi = {10.1109/ICHMS53169.2021.9582448}, keywords = {interviews, thematic analysis, intelligent cockpit assistant systems, human-AI interaction, imperfect AI}, url = {https://doi.org/10.1109/ICHMS53169.2021.9582448}, } @inproceedings{, author = {Gampig, Jonas and Terzimehić, Tarik and Dorofeev, Kirill}, title = {PLC Integration into Industry 4.0 Middleware: Function Block Library for the Interaction with REST and OPC UA Asset Administration Shells}, booktitle = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, publisher = {IEEE}, journal = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, year = {2021}, month = sep, abstract = {An asset administration shell (AAS), as a key concept of Industry 4.0 (I4.0), provides a machine-accessible interface to any kind of asset. To enable interoperability and smooth integration of the devices into the I4.0 middleware, an application implementing the device's functionality should be able to interact with different AASs. In this work, we investigate the integration of the Programmable Logic Controller (PLC) runtime systems into the I4.0 middleware. For doing this, we specify the function blocks (FBs) for connecting the PLCs with AASs and other I4.0 components, such as registry and discovery server. We analyze the requirements of such FBs while focusing on REST/HTTP- and OPC UA-based AASs, and provide interface specification for IEC 61499- and IEC 61131-3-based FBs. Furthermore, we implemented an FB library that enables communication with an AAS from the respective control applications. Those FBs allow accessing properties and invoking operations of remote AASs, as well as hosting AASs submodels. Common functionalities, such as registering the runtime system at the registry component, or finding AASs, are also supported. The results obtained in this paper will ease interaction with the complex AAS structure from the low-level devices.}, doi = {10.1109/ETFA45728.2021.9613267}, keywords = {Industry 4.0, model-based systems engineering, MbSE, IEC 61499, IEC 61131-3, asset administration shell, digital twin, PLC, OPC UA, REST}, } @inproceedings{, author = {Terzimehić, Tarik and Dorofeev, Kirill and Bergemann, Sebastian and Zoitl, Alois and Voss, Sebastian}, title = {Towards Service Deployment and Composition in Industry 4.0}, booktitle = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, publisher = {IEEE}, journal = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, year = {2021}, month = sep, abstract = {The fourth industrial revolution (Industry 4.0) anticipates unplanned changes of production processes. Production changes may trigger synthesis, and preferably optimization, of architecture-level decisions, such as service deployment and composition. Performing such architecture-level decisions manually is difficult due to the ever-rising complexity of Industry 4.0 systems. In order to (semi-)automate the architecture synthesis and optimization, we propose an approach of service deployment and composition by using existing domain models. Our contribution is threefold: (1) We suggest a workflow with domain models for architecture synthesis in the industrial automation. (2) We display the formalization on a part of the workflow and provide an initial prototype of service deployment synthesis using a satisfiability modulo theories (SMT) solver. (3) We envision a way of service composition and code generation, and prototypically implemented it as conclusion of the suggested workflow. We demonstrate the practical use of the proposed approach in the Industry 4.0 scenario, i.e., flexible production of new products.}, doi = {10.1109/ETFA45728.2021.9613327}, keywords = {Industry 4.0, IEC 61499, deployment synthesis, service composition, code generation, model-based systems engineering, MbSE, design-space exploration, DSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Gallina, Barbara and Soima, Liana}, title = {Safety Case Maintenance: A Systematic Literature Review}, booktitle = {Proceedings of the 40th International Conference on Computer Safety, Reliability and Security ({SAFECOMP})}, publisher = {Springer, Cham}, series = {LNCS}, volume = {12852}, pages = {115--129}, year = {2021}, month = aug, abstract = {Safety standards from different domains recommend the execution of a process for keeping the system safety case up to date, whenever the system undergoes a change, however, without providing any more specific guidelines on how to do this. Even if several (semi)automated safety case maintenance approaches have been proposed in the literature, currently, in the industry, the execution of this process is still manual, being error prone and expensive. To this end, we present in this paper the results of what is, to the best of our knowledge, the first Systematic Literature Review (SLR) conducted with the goal to provide a holistic overview of state-of-the-art safety case maintenance approaches. For each identified approach, we analyze its strengths and weaknesses. We observe that existing approaches are pessimistic, identifying a larger number of safety case elements as impacted by a change than the number of the actually impacted elements. Also, there is limited quantitative impact assessment. Further, existing approaches only address a few system change scenarios when providing guidelines for updating the safety case.}, doi = {10.1007/978-3-030-83903-1_8}, keywords = {Safety case maintenance, Systematic literature review, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Beyene, Tewodros and C{\^{a}}rlan, Carmen}, title = {{CyberGSN}: A Semi-formal Language for Specifying Safety Cases}, booktitle = {Proceedings of the 51st Annual {IEEE/IFIP} International Conference on Dependable Systems and Networks Workshops ({DSN-W})}, publisher = {IEEE}, year = {2021}, month = jun, abstract = {The use of safety cases to explicitly present safety considerations and decisions is a common practice in the safety-critical domain. A safety case can be used to scrutinize the safety assessment approach used by practitioners internally, or as an input for the certification process for an external certifying authority. However, safety cases are still created manually to explicate the followed safety assessment and assurance measures. In addition, although safety cases may be created in a modular way by multiple entities, and it may be critical for each entity to digitally sign its part of the assurance for accountability, the common notations are not expressive enough to include the notion of entity. Especially in cyber-security applications, the notion of entity is very critical. In this paper, we propose a formal logic based language called CyberGSN, with an explicit notion of entity, that can be used for specifying safety cases and safety case patterns, enabling the automated creation and maintenance of safety cases.}, doi = {10.1109/DSN-W52860.2021.00021}, keywords = {Safety Case, Pattern, Entity, Decentralization, Model-based Systems Engineering, MbSE}, } @article{, author = {Ratiu, Daniel and Nordmann, Arne and Munk, Peter and C{\^{a}}rlan, Carmen and Voelter, Markus}, title = {{FASTEN}: An Extensible Platform to Experiment with Rigorous Modeling of Safety-Critical Systems}, booktitle = {Domain-Specific Languages in Practice}, publisher = {Springer, Cham}, journal = {Domain-Specific Languages in Practice}, pages = {131--164}, year = {2021}, month = apr, abstract = {The increasing complexity of safety-critical systems and the shorter time-to-market requires a high degree of automation during all development phases from requirements specification to design, implementation, verification, and safety assurance. To make this feasible, we need to describe different system aspects using appropriate models that are semantically rich and, whenever possible, formally defined such that they are verifiable by automated methods. At the same time, they must be easy to understand by practitioners and must allow them to capture the domain concepts with minimal encoding bias. In this chapter, we describe FASTEN, an open-source research environment for model-based specification and design of safety-critical systems using domain-specific languages. FASTEN enables the experimentation with modeling abstractions at different levels of rigor and their integration in today’s development processes. We present an overview of the currently available domain-specific languages (DSLs) used to formally specify requirements, system designs, and assurance arguments. These DSLs have been developed and used in technology transfer projects by researchers from different organizations—Siemens, Bosch, fortiss, and itemis. Last but not least, we discuss lessons learned from implementing the languages and interacting with practitioners and discuss the language engineering features of MPS that enabled our approach and its open challenges.}, isbn = {978-3-030-73758-0}, doi = {10.1007/978-3-030-73758-0_5}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Petrovska, Ana and Neuss, Malte and Bergemann, Sebastian and B{\"{u}}chner, Martin and Shohab, Ansab}, title = {Smart Self-Adaptive Cyber-Physical Systems: How can Exploration and Learning Improve Performance in a Partially Observable Multi-Agent Context?}, booktitle = {ADAPTIVE 2021: The Thirteenth International Conference on Adaptive and Self-Adaptive Systems and Applications}, year = {2021}, month = apr, timestamp = 2021.04.18, abstract = {Cyber-physical systems (CPSs) are software-intensive systems that are embedded in the physical world to monitor, control and coordinate a variety of processes in both the physical and the digital world. As a result, they often operate in complex, dynamic, and unanticipated environments with various potential sources of run-time changes and uncertainties, that could potentially lead the CPSs to faults, and even to complete system failures. To cope with these changes, the systems should have the capabilities to self-adapt in order to continue meeting their functional specifications. In this paper, we investigate how creating self-adaptive CPSs which are able to collaborate and learn in a dynamic, partially observable, multi-agent context, can not only preserve but also improve the performance, despite all the changes introduced to the system at run-time. We evaluate the proposed methodology on an in-house developed, multi-agent system from the robotics domain.}, isbn = {978-1-61208-848-8}, issn = {2308-4146}, keywords = {self-adaptive systems, cyber-physical systems, collaboration, learning, partial observability, Model-based Systems Engineering, MbSE}, url = {https://www.thinkmind.org/index.php?view=article&articleid=adaptive_2021_1_10_50002}, } @inproceedings{, author = {Wozniak, Ernest and Putzer, Henrik J. and C{\^{a}}rlan, Carmen}, title = {{AI}-Blueprint for Deep Neural Networks}, booktitle = {Proceedings of the Workshop on Artificial Intelligence Safety ({SafeAI} '21)}, publisher = {{CEUR}}, volume = {2808}, year = {2021}, month = feb, abstract = {Development of trustworthy (e.g., safety and/or security critical) hardware/software-based systems needs to rely on well-defined process models. However, engineering trustworthy systems implemented with artificial intelligence (AI) is still poorly discussed. This is, to large extend, due to the standpoint in which AI is a technique applied within software engineering. This work follows a different viewpoint in which AI represents a 3rd kind technology (next to software and hardware), with close connections to software. Consequently, the contribution of this paper is the presentation of a process model, tailored to AI engineering. Its objective is to support the development of trustworthy systems, for which parts of their safety and/or security critical functionality are implemented with AI. As such, it considers methods and metrics at different AI development phases that shall be used to achieve higher confidence in the satisfaction of trustworthiness prop- erties of a developed system.}, keywords = {Safety Case, Model-based Systems Engineering, MbSE}, url = {http://ceur-ws.org/Vol-2808/Paper_22.pdf}, } @inproceedings{Dieudonne2021RMC, author = {Dieudonne, Laurent and Bayha, Andreas and M{\"{u}}ller, Benedikt}, title = {{RMC} Factory: A New Approach for Avionics Software Reuse}, booktitle = {3rd Workshop on Avionics Systems and Software Engineering ({AvioSE21}, {SE} 2021 Satellite Events)}, publisher = {CEUR-WS}, volume = {2814}, year = {2021}, month = feb, abstract = {In contrast to many other industries, the reuse-rate of software in the avionics domain is very low. This situation originates mainly from the incomplete specifications for reuse in the avionics standards. In particular, these ones address almost exclusively the reuse of certified software previously developed for a specific project and consider only big monolithic executable components like complete applications or operating system modules. This paper describes a new approach enabling an efficient reuse of components from small up to big scale, specifically developed for reuse and conceived to fulfill the fundamentals DO-178C requirements while maximizing the reuse of certification artefacts. This presented approach combines methods, tool infrastructure and process extensions and we denote it as Reusable Modular Component (RMC) Factory. We also resent an implementation of the tool infrastructure and discuss our lessons learned from this mplementation and the first experiments.}, keywords = {Model-based Systems Engineering, MbSE, Avionics, component, reuse, RMC, software factory, certification, process, tool chain}, url = {http://ceur-ws.org/Vol-2814/paper-A4-2.pdf}, } @inproceedings{, author = {Jahić, Jasmin and Diewald, Alexander}, title = {Handling Concurrency in Embedded Software System from Architectural Point of View}, booktitle = {HiPEAC conference}, year = {2021}, month = jan, timestamp = 2021.01.19, address = {Tutorials}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://jahic.github.io/hipeac2021}, } @inbook{, author = {B{\"{o}}hm, Birthe and C{\^{a}}rlan, Carmen and Sohr, Annelie and Unverdorben, Stephan and Vollmar, Jan}, editor = {B{\"{o}}hm, Wolfgang and Broy, Manfred and Klein, Cornel and Pohl, Klaus and Rumpe, Bernhard and Schr{\"{o}}ck, Sebastian}, title = {Architectures for Flexible Collaborative Systems}, booktitle = {Model-Based Engineering of Collaborative Embedded Systems}, publisher = {Springer International Publishing}, journal = {Model-Based Engineering of Collaborative Embedded Systems}, pages = {49--70}, year = {2020}, month = dec, timestamp = 2020.12.15, abstract = {Collaborative systems are characterized by their interaction with other systems in collaborative system groups in order to reach a common goal. These systems interact based on fixed rules and have the ability to change structurally, if necessary. Changes in the collaboration are usually triggered from outside and are time-discrete with a rather wide time scale. The architectures of these systems and system groups must support flexibility and adaptability at runtime while also ensuring specific qualities, although these changes and their consequences cannot be fully foreseen in all combinations at design time. In order to enable knowledge preservation and reuse for the design of system architectures for flexible collaborative systems and system groups, we present a method for designing reference architectures for systems and system groups. For this approach, we present an example of a reference architecture for an operator assistance system. To adequately consider safety requirements during the design, we further introduce a method which adapts safety argumentation for flexible collaborative systems to changes in their specification or operating context.}, isbn = {978-3-030-62136-0}, doi = {10.1007/978-3-030-62136-0_3}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Gallina, Barbara}, title = {Enhancing State-of-the-art Safety Case Patterns to Support Change Impact Analysis}, booktitle = {Proceedings of the 30th European Safety and Reliability Conference (ESREL-2020)}, year = {2020}, month = nov, abstract = {The new generation of safety-critical systems will be interconnected, having other systems as collaborating partners for achieving common goals (e.g., interconnected cyber-physical systems such as connected cars, or collaborative embedded systems such as an advanced driver assistance system connected with different sensors). Frequent new business goals of such systems are to enable new collaborations with new types of technical systems, thus changing their operating context, which triggers the need for agile development in automotive. In safety-critical domains, a change in the operating context triggers the need for impact analysis on the artefacts generated during the safety lifecycle. Impact analyses are time and resource consuming, hindering agile development. Hence, the need for automation. Safety cases comprise safety arguments explicitly specifying the traces among the artefacts generated during the safety lifecycle. Our longer term goal is to support the automated identification of the artefacts affected by changes in the system's operating context, while proposing an automated change impact analysis executed on the system's safety case. To ensure completeness of the results of such analysis, in this work, we enhance state-of-the-art safety case patterns by referencing all artefacts generated during the safety lifecycle. Further, we enable the explicit specification of the properties of the operating context for which we foresee certain changes. We evaluate our patterns by using them for the construction of the safety case of a simplified airbag system.}, doi = {10.3850/978-981-14-8593-0_4672-cd}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Petrișor, Daniel and Gallina, Barbara and Schoenhaar, Hannes}, title = {Checkable Safety Cases: Enabling Automated Consistency Checks between Safety Work Products}, booktitle = {Proceedings of the 10th IEEE International Workshop on Software Certification (WoSoCer) co-located with ISSRE}, publisher = {IEEE}, year = {2020}, month = oct, keywords = {Model-based systems engineering, MbSE}, url = {https://sites.google.com/view/wosocer2020}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Ratiu, Daniel}, title = {{FASTEN.Safe}: A Model-Driven Engineering Tool to Experiment with Checkable Assurance Cases}, booktitle = {Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP)}, publisher = {Springer}, series = {LNCS}, volume = {12234}, pages = {298--306}, year = {2020}, month = sep, abstract = {The Goal Structuring Notation (GSN) is popular among safety engineers for modeling assurance cases. GSN elements are specified using plain natural language text, this giving safety engineers great flexibility to express their arguments. However, pure textual arguments introduce ambiguities and prevent automation. Currently, assurance cases are verified by manual reviews, which are error prone, time consuming, and not adequate for today’s systems complexity and agile development methodologies. In this paper we present our research tool FASTEN.Safe, which extends GSN with a set of higher-level modeling language constructs capturing recurring argumentation patterns and integrating formal system models. This allows automatically checking 1) the intrinsic consistency of assurance models, 2) the consistency of arguments with system models and 3) the verification of safety claims themselves by using external verification tools. FASTEN.Safe is open source and allows experimenting with language abstractions to bridge the world of GSN-based arguments that are common among safety engineers and the world of formal methods that enable automation. Last but not least, we report on the preliminary experience gained with FASTEN.Safe.}, doi = {10.1007/978-3-030-54549-9_20}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{, author = {Wozniak, Ernest and C{\^{a}}rlan, Carmen and Acar-Celik, Esra and Putzer, Henrik J.}, title = {A Safety Case Pattern for Systems with Machine Learning Components}, booktitle = {Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP)}, publisher = {Springer}, series = {LNCS}, volume = {12235}, pages = {370--382}, year = {2020}, month = sep, abstract = {Several standards from the domain of safety critical systems, in order to support the argumentation of the safety assurance of a system under development, recommend the construction of a safety case. This activity is guided by the objectives to be met, recommended or required by the standards along the safety lifecycle. Ongoing attempts to use Machine Learning (ML) for safety critical functionality revealed certain deficits. For instance, the widely recognized standard for functional safety of automotive systems, ISO 26262, which can be used as a basis to construct a safety case, does not reason about ML. To this end, the goal of this work is to provide a pattern for arguing about the correct implementation of safety requirements in system components based on ML. The pattern is integrated within an overall encompassing approach for safety case generation for automotive systems and its applicability is showcased on a pedestrian avoidance system.}, doi = {10.1007/978-3-030-55583-2_28}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{, author = {Gomes, Cl{\'{a}}udio and Thule, Casper and L{\'{u}}cio, Levi and Vangheluwe, Hans and Larsen, Peter Gorm}, title = {Generation of Co-simulation Algorithms Subject to Simulator Contracts}, booktitle = {Software Engineering and Formal Method (SEFM 2019)}, publisher = {Springer, Cham}, series = {LNCS}, volume = {12226}, year = {2020}, month = sep, abstract = {Correct co-simulation results require a careful consideration of how the interacting simulators are implemented. In version 2.0 of the FMI Standard, input handling implementation is left implicit, which leads to the situation where a simulator can be interacted with in a manner that its implementation does not expect, yielding incorrect results. In this paper, we build on prior work to make information about each simulator implementation explicit, in order to derive correct interactions with it. The formalization we use is specific to two kinds of contracts, but could serve as a basis to a general approach to black box co-simulation. The algorithm we propose generates a co-simulation execution plan in linear time. It has been successfully applied to an industrial case study, and the results are available online.}, isbn = {978-3-030-57506-9}, doi = {10.1007/978-3-030-57506-9_4}, keywords = {Co-simulation, Prolog, Contract-based code generation, Constraint solving, Model-based Systems Engineering, MbSE}, } @misc{, author = {Bayha, Andreas and Aravantinos, Vincent}, title = {Generic Analysis of Model Product Lines via Constraint Lifting}, year = {2020}, month = aug, abstract = {Engineering a product-line is more than just describing a product-line: to be correct, every variant that can be generated must satisfy some constraints. To ensure that all such variants will be correct (e.g. well-typed) there are only two ways: either to check the variants of interest individually or to come up with a complex product-line analysis algorithm, specific to every constraint. In this paper, we address a generalization of this problem: we propose a mechanism that allows to check whether a constraint holds simultaneously for all variants which might be generated. The contribution of this paper is a function that assumes constraints that shall be fulfilled by all variants and generates ("lifts") out of them constraints for the product-line. These lifted constraints can then be checked directly on a model product-line, thus simultaneously be verified for all variants. The lifting is formulated in a very general manner, which allows to make use of generic algorithms like SMT solving or theorem proving in a modular way. We show how to verify lifted constraints using SMT solving by automatically translating model product-lines and constraints. The scalability of the approach is demonstrated with an industrial case study, in which we apply our lifting to a domain specific modeling language of the manufacturing domain.}, howpublished = {arXiv:2008.11427 [cs.SE]}, doi = {10.48550/arXiv.2008.11427}, keywords = {Model-based Systems Engineering, MbSE}, } @article{, author = {Eder, Johannes and Voss, Sebastian and Bayha, Andreas and Ipatiov, Alexandru and Khalil, Maged}, title = {Hardware architecture exploration: automatic exploration of distributed automotive hardware architectures}, journal = {Software and Systems Modeling}, volume = {19}, pages = {911--934}, year = {2020}, month = jul, abstract = {As the engineering of distributed embedded systems is getting more and more complex, due to increasingly sophisticated functionalities demanding more and more powerful hardware, model-based development of software-intensive embedded systems has become a de facto standard in recent years. Among other advantages, it enables design space exploration methods allowing for frontloading techniques which support a system architect already at early stages of development. In this paper, we want to present an approach which is capable of automatically generating automotive E/E architectures (electric/electronic architecture; in-car network of processing units and buses). Based on the concept of viewpoints, we will introduce dedicated technical meta-models, a language to formally describe a hardware architecture exploration problem and an automatic exploration approach using satisfiability modulo theories. We will furthermore introduce a dedicated methodology and show how an exploration integrates into a system development process. In the end, we will evaluate our approach by applying it to an industrial use case provided by Continental.}, doi = {10.1007/s10270-020-00786-6}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, deployment synthesis, HW/SW co-design, model-based systems engineering, MbSE, case study}, } @article{bayha2020Describing, author = {Bayha, Andreas and Bock, J{\"{u}}rgen and Boss, Birgit and Diedrich, Christian and Malakuti, Somayeh}, title = {Describing Capabilities of {Industrie 4.0} Components}, journal = {German Electrical and Electronics Manufacturers Association, Frankfurt am Main, Germany}, year = {2020}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://www.plattform-i40.de/IP/Redaktion/DE/Downloads/Publikation/Capabilities_Industrie40_Components.html}, } @article{Perzylo2019b, author = {Perzylo, Alexander and Grothoff, Julian and L{\'{u}}cio, Levi and Weser, Michael and Malakuti, Somayeh and Venet, Pierre and Aravantinos, Vincent and Deppe, Torben}, title = {Capability-based semantic interoperability of manufacturing resources: A {BaSys} 4.0 perspective}, journal = {IFAC-PapersOnLine}, volume = {52}, number = {13}, pages = {1590--1596}, year = {2019}, month = dec, note = {{IFAC} Conference on Manufacturing Modeling, Management, and Control ({MIM})}, abstract = {In distributed manufacturing systems, the level of interoperability of hardware and software components depends on the quality and flexibility of their information models. Syntactic descriptions of input and output parameters, e.g., using interface description languages (IDL), are not suffcient when it comes to evaluating whether a manufacturing resource provides the capabilities that are required for performing a particular process step on a product. The semantics of capabilities needs to be explicitly modelled and must be provided together with manufacturing resources. In this paper, we introduce concepts developed by the German BaSys 4.0 initiative dealing with semantically describing manufacturing skills, orchestrating higher-level skills from basic skills, and using them in a cognitive manufacturing framework.}, doi = {10.1016/j.ifacol.2019.11.427}, keywords = {robotics, basys 4.0, model-based systems engineering, MbSE}, } @inproceedings{8869083, author = {Walzel, Hendrik and Vathoopan, Milan and Zoitl, Alois and Knoll, Alois}, title = {An Approach for an Automated Adaption of KPI Ontologies by Reusing Systems Engineering Data}, booktitle = {2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)}, pages = {1693-1696}, year = {2019}, month = sep, abstract = {Technological progress leads to an increased utilization of data analysis and Business Intelligence that support manufacturing management decisions. Many promising solutions utilize semantic technologies. However, the deployment and maintenance of semantic technologies especially in reconfigurable manufacturing environments require a lot of manual effort. Concepts to embed them in an automated environment, as required by Reconfigurable Manufacturing Systems, are limited. In this paper, we present an approach to reuse systems engineering data to guide an automated process that updates a production data knowledge base. Thereby, an ontology that integrates distributed operational data to compute Key Performance Indicators such as the Overall Equipment Effectiveness index can be updated during the manufacturing reconfiguration process. This reduces the effort to handle the required changes of semantic data integration systems and enables a cost-effective adaption of the Business Intelligence for Reconfigurable Manufacturing Systems.}, doi = {10.1109/ETFA.2019.8869083}, keywords = {Semantics;Modeling;Knowledge based systems;Ontologies;Manufacturing systems;reconfigurable manufacturing systems;semantic data integration;KPI;OEE;systems engineering}, } @inproceedings{, author = {Terzimehić, Tarik and Bayha, Andreas and Dorofeev, Kirill}, title = {Function Blocks for the Interaction with the Asset Administration Shell}, booktitle = {Proceedings of the {IEEE} International Conference on Emerging Technologies And Factory Automation ({ETFA})}, year = {2019}, month = sep, abstract = {An asset administration shell (AAS), as a key concept of the Industry 4.0, provides a machine accessible interface to any kind of asset. An application implementing the devices functionality should be able to interact with different AASs. In this work, we specify the function blocks (FBs) for accessing properties and invoking operations of AASs. We analyzed the nature and requirements of such FBs while focusing on REST/HTTP- and OPC UA-based AASs and provided IEC 61499-based implementation. The expected outcome of this paper will ease an interaction with the complex AAS structure from the low-level devices.}, doi = {10.1109/ETFA.2019.8868995}, keywords = {Industry 4.0, IEC 61499, IEC 61131-3, asset administration shell, digital twin, PLC, OPC UA, REST, model-based systems engineering, MbSE}, } @inproceedings{, author = {Gomes, Cl{\'{a}}udio and L{\'{u}}cio, Levi and Vangheluwe, Hans}, title = {Semantics of Co-simulation Algorithms with Simulator Contracts}, booktitle = {2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)}, publisher = {IEEE}, pages = {784--798}, year = {2019}, month = sep, abstract = {The rapid adoption of co-simulation techniques allows for holistic complex system development. However, ensuring trustworthy results when combining simulators requires a careful consideration of their implementation and capabilities. Especially in black box integration, these are frequently left implicit. In this paper, we explore a way to account for simulator capabilities, by formalizing the execution of a co-simulation that respects such contracts. This formalization is specific to two kinds of contracts, but could serve as a basis to a general approach to black box co-simulation. An example application of the semantics to generate master algorithms is presented.}, doi = {10.1109/MODELS-C.2019.00124}, keywords = {co-simulation, prolog, contract-based-design, constraint-solving, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Terzimehić, Tarik and Wenger, Monika and Voss, Sebastian and Gr{\"{u}}ner, Sten and Elfham, Haitham}, title = {SMT-Based Deployment Calculation in Industrial Automation Domain}, booktitle = {Proceedings of the {IEEE} International Conference on Emerging Technologies And Factory Automation ({ETFA})}, publisher = {IEEE}, year = {2019}, month = sep, abstract = {The desired flexibility of industrial automation systems foresees among others flexible deployment and execution of control applications on distributed control nodes. This task can be performed more efficiently by an automated deployment algorithm yielding a valid deployment and optimizing nonfunctional objectives. Although extensively investigated, automated deployment approaches for the automotive domain cannot be translated to industrial control applications, due to a different execution semantics. Thus, in this paper, we present a method of satisfiability modulo theories (SMT)-based automated deployment of the industrial automation systems. We formalize and implement domain-relevant constraints and objectives. Our contribution is threefold: 1) we formalize the functional coupling and end-to-end deadline constraints and objectives while considering the semantics of control applications, 2) we encode the deployment problem into an SMT form, and 3) we validate the approach on an abstract example and a domain-relevant use case. The results obtained in this paper will allow application engineers to fulfill functional and real-time requirements by automatically solving the deployment problem.}, doi = {10.1109/ETFA.2019.8868247}, keywords = {BaSys 4.0, Model-based systems engineering, MbSE, deployment, Industry 4.0, IEC 61499, SMT, E2E latency, functional coupling, design-space exploration, DSE}, } @article{, author = {Bures, Tomas and Weyns, Danny and Schmerl, Bradley and Fitzgerald, John and Aniculaesei, Adina and Berger, Christian and Cambeiro, Joao and Carlson, Jan and Chowdhury, Shafiul Azam and Daun, Marian and Li, Nianyu and Markthaler, Matthias and Menghi, Claudio and Penzenstadler, Birgit and Pettit, Aedan and Pettit, Robert and Sabatucci, Luca and Tranoris, Christos and Vangheluwe, Hans and Voss, Sebastian and Zavala, Edith}, title = {Software Engineering for Smart Cyber-Physical Systems ({SEsCPS} 2018) - Workshop Report}, publisher = {ACM}, journal = {SIGSOFT Softw. Eng. Notes}, volume = {44}, number = {4}, pages = {11--13}, year = {2019}, month = sep, address = {New York, NY, USA}, abstract = {Smart Cyber-Physical Systems (sCPS) are a novel kind of Cyber- Physical System engineered to take advantage of large-scale cooperation between devices, users and environment to achieve added value in the face of uncertainty and changing environments. Examples of sCPS include modern traffic systems, Industry 4.0 systems, systems for smart buildings, and smart energy grids. The uniting aspect of all these systems is that to achieve their high level of intelligence, adaptivity and ability to optimize and learn, they rely heavily on software. This makes them software-intensive systems, where software becomes their most complex part. Engineering sCPS thus becomes a recognized software engineering discipline, which, due to specifics of sCPS, can only partially rely on the existing body of knowledge in software engineering. In fact, it turns out that many of the traditional approaches to architecture modeling and software development fall short in their ability to cope with the high dynamicity and uncertainty of sCPS. This calls for innovative approaches that jointly reflect and address the specifics of such systems. This paper maps the discussions and results of the Fourth International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS 2018), which focuses on challenges and promising solutions in the area of software engineering for sCPS.}, issn = {0163-5948}, doi = {10.1145/3364452.3364465}, keywords = {cyber-physical systems, software engineering, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Gavrilenko, Natalia and Ponce de Le{\'{o}}n, Hern{\'{a}}n and Furbach, Florian and Heljanko, Keijo and Meyer, Roland}, title = {{BMC} for Weak Memory Models: Relation Analysis for Compact {SMT} Encodings}, booktitle = {Computer Aided Verification ({CAV}) 2019.}, publisher = {Springer, Cham}, series = {LNCS}, volume = {11561}, year = {2019}, month = jul, abstract = {We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.}, isbn = {978-3-030-25540-4}, doi = {10.1007/978-3-030-25540-4_19}, keywords = {Weak memory models, CAT, Concurrency, BMC, SMT, Model-based Systems Engineering, MbSE}, } @inproceedings{Diewald2019, author = {Diewald, Alexander and Barner, Simon and Saidi, Selma}, title = {Combined Data Transfer Response Time and Mapping Exploration in MPSoCs}, booktitle = {10th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems ({WATERS}) co-located with {ECRTS}}, year = {2019}, month = jul, abstract = {Recent embedded applications such as Autonomous Driver Assistance Systems (ADAS) require large computational resources that increase the need for HW accelerators, e.g., in system-on-chip-based platforms. Synthesising optimal task/data mappings and schedules for such platforms becomes increasingly challenging, even more in safety-critical contexts. For designing real-time heterogeneous systems, response time computation and the resolution of task mapping problems are required as demanded in the WATERS 2019 challenge. Our contribution to address the challenge is to extend a design space exploration (DSE) formulation of mapping applications on MPSoCs architectures to consider DMA-based data (pre)-fetching. The approach is performed in two steps. First, we determine task mappings to a heterogeneous MPSoC platform using a multi-objective evolutionary algorithm (MOEA)-based DSE. In order to check the feasibility of an allocation, and to rate its quality, we use a SMT solver to construct schedules whose latency is close to the achievable minimum. Our task response time analysis considers the effects of memory access times and DMAs to supply the SMT scheduler with data fetching latencies. The MOEA-DSE, the SMT scheduler, and the response time calculation are integrated into the AutoFOCUS 3 tool that has been extended with an importer for the AMALTHEA model that specifies the challenge use case.}, howpublished = {10th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems ({WATERS}) co-located with {ECRTS}}, keywords = {AutoFOCUS3, design-space exploration, DSE, deployment synthesis, mapping, model-based systems engineering, MbSE}, url = {https://archives.ecrts.org/fileadmin/WebsitesArchiv/ecrts2019/waters/waters-program/}, } @inproceedings{, author = {bin Abid, Saad and Mahajan, Vishal and L{\'{u}}cio, Levi}, title = {Towards Machine Learning for Learnability of MDD Tools}, booktitle = {Software Engineering and Knowledge Engineering (SEKE) Conference, Lisbon, Portugal}, pages = {1--6}, year = {2019}, month = jul, location = {Lisbon, Portugal}, abstract = {Learning how to build software systems using new tools can be a daunting task to anyone new to the job. This is especially true of tools that provide a large number of functionalities and views on the system under development, such as IDES for Model-Driven Development (MDD). Applying Machine Learning (ML) techniques can help in this state of affairs by pointing out to appropriate next actions to rookie or even intermediate developers. AutoFOCUS3 (AF3) is a mature MDD tool we are building in-house and for which we provide regular tutorials to new users. These users come from both the academia (e.g, students/professors) and the industry (e.g. managers/software engineers). Nonetheless, AF3 remains a complex tool and we have found there is a need to speedup the learning curve of the tool for students that attend our tutorials-or alternatively and more importantly for others that simply download the tool and attempt using it without human supervision. In this paper, we describe a machine learning-based recommendation system named MAGNET for aiding beginner and intermediate users of AF3 in learning the tool. We describe how we have gathered data and trained an ML model to suggest new commands, how a recommender system was integrated in the AF3, experiments we have run thus far, and the future directions of our work.}, doi = {10.18293/SEKE2019-050}, keywords = {Model-Driven Development, MDD, AutoFOCUS3, Machine Learning, Intelligent Recommendation Systems, IRS, Eclipse IDE, Domain-Specific Languages , DSLs, development interaction data, methodology, tooling, model-based systems engineering, MbSE}, } @inproceedings{, author = {Zverlov, Sergey and Voss, Sebastian and B{\"{o}}hm, Thomas and Herpel, Hans-J{\"{u}}rgen and Kerep, Mladen}, title = {Model-based methodology for space vehicles}, booktitle = {Proceedings of the Eurospace Annual Conference on Data Systems in Aerospace (DASIA)}, year = {2019}, month = jun, abstract = {The technological challenges that companies in the space domain are facing today are becoming more and more complex. On the one hand complexity of the tasks that need to be performed by the new generation of spacecrafts is increasing. On the other hand, the development needs to be cost and time efficient to be able to compete against new players in this domain, such as SpaceX. To deal with these challenges new development tools and methods are needed. In scope of this work we propose a model-based approach for future spacecrafts. We integrated this approach into a state-of-the-art model-based tool and applied it onto an industrial case-study to show proof-of-concept.}, keywords = {AutoFOCUS3, case study, model-based systems engineering, MbSE}, } @inproceedings{Kraemmer2019a, author = {Kr{\"{a}}mmer, Annkathrin and Sch{\"{o}}ller, Christoph and Gulati, Dhiraj and Knoll, Alois}, title = {Providentia - A Large Scale Sensing System for the Assistance of Autonomous Vehicles}, booktitle = {Robotics Science and Systems Workshops ({RSS} Workshops)}, publisher = {RSS Foundation}, year = {2019}, month = jun, address = {Freiburg, Germany}, abstract = {The environmental perception of autonomous vehicles is not only limited by physical sensor ranges and algorithmic performance, but also occlusions degrade their understanding of the current traffic situation. This poses a great threat for safety, limits their driving speed and can lead to inconvenient maneuvers that decrease their acceptance. Intelligent Transportation Systems can help to alleviate these problems. By providing autonomous vehicles with additional detailed information about the current traffic in form of a digital model of their world, i.e. a digital twin, an Intelligent Transportation System can fill in the gaps in the vehicle's perception and enhance its field of view. However, detailed descriptions of implementations of such a system and working prototypes demonstrating its feasibility are scarce. In this work, we propose a hardware and software architecture to build such a reliable Intelligent Transportation System. We have implemented this system in the real world and show that it is able to create an accurate digital twin of an extended highway stretch. Furthermore, we provide this digital twin to an autonomous vehicle and demonstrate how it extends the vehicle's perception beyond the limits of its on-board sensors.}, keywords = {Intelligent Transportation Systems, Autonomous Driving, Robotics}, url = {https://sites.google.com/view/uad2019/accepted-posters}, } @article{, author = {Syriani, Eugene and Sousa, Vasco and L{\'{u}}cio, Levi}, title = {Structure and behavior preserving statecharts refinements}, journal = {Science of Computer Programming}, volume = {170}, pages = {49--79}, year = {2019}, month = jan, abstract = {Statecharts are one of the most popular modeling formalisms that is used in a diversity of real world applications, such as cyber-physical systems, mobile computing, and bio-informatics. Following common step-wise refinement strategies, modelers often develop and evolve Statecharts models incrementally to satisfy requirements and changes. Although there are already several existing Statecharts refinement approaches, they provide insufficient guarantees to support reasoning about the preservation of both its internal structure, to enhance development and maintenance, and its behavior, which external components using the Statecharts model may depend on. In this paper, we formulate formal requirements to minimally limit the allowable Statecharts refinement operations such that certain assumptions on the structure and reachability of the Statecharts model will hold. To satisfy these requirements, we propose a set of practical bounding refinement rules that allows the modeler to achieve such refinements for which notions of behavior and structure preservation can be statically verified under some assumptions. Our implementation shows how these rules can be applied in realistic scenarios.}, doi = {10.1016/j.scico.2018.10.005}, keywords = {Statechart, Refinement, Software design, Verification, Model-based Systems Engineering, MbSE}, } @article{, author = {Libal, Tomer and Volpe, Marco}, title = {A general proof certification framework for modal logic}, booktitle = {Mathematical Structures in Computer Science}, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, volume = {29}, number = {8}, pages = {1344--1378}, year = {2019}, abstract = {One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labelled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.}, doi = {10.1017/S0960129518000440}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Kanav, Sudeep and L{\'{u}}cio, Levi and Hilden, Christian and Schuetz, Thomas}, title = {Design and Runtime Verification Side-by-Side in eTrice}, booktitle = {Proceedings of the {NASA} Formal Methods Symposium}, publisher = {Springer}, series = {LNCS}, volume = {11460}, pages = {255--262}, year = {2019}, abstract = {eTrice is a mature open-source model-based software engineering tool, based on the ROOM methodology. It is currently used in the industry for the development of solutions for domains such as health, heavy machinery and the automotive. eTrice natively incorporates mechanisms for runtime verification. At the request of the developers of eTrice, we have incorporated model checking in their tool chain, by partly reusing the existing runtime verification architecture. We report on the implementation of the tool, experiments that we conducted, and lessons learned regarding the synergies between the two verification techniques.}, doi = {10.1007/978-3-030-20652-9_17}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{carlan19wosocer, author = {Nigam, Vivek and Tsalidis, Alexandros and Voss, Sebastian and C{\^{a}}rlan, Carmen}, title = {ExplicitCase: Tool-support for Creating and Maintaining Assurance Arguments Integrated with System Models}, booktitle = {2019 IEEE International Symposium on Software Reliability Engineering Workshops ({ISSREW})}, year = {2019}, abstract = {Assurance cases are collections of standard-mandated documents that entail the specification of system's objectives and a collection of processes, development or verification evidence regarding the satisfaction of the respective objectives. A considerable amount of work has been done in the direction of modelling assurance cases, to support communication and reasoning regarding the system's safety. In this work, we present a set of features of ExplicitCase - a tool for modeling assurance cases. While there is a plethora of tools for creating and managing model-based assurance cases, the uniqueness of our tool is that it integrates assurance case models with system models created in AutoFOCUS3 (AF3) - an open-source model-based development tool for embedded software systems. While trying to keep up with state-of-the-art assurance case editors, the newly implemented features support assurance case creation using typed patterns, change impact analysis for assurance cases, assessment of the confidence in the created assurance arguments, export of the argumentation diagrams generated in ExplicitCase and integration of assurance case models with system models created in AutoFOCUS3. In particular, based on the integration with AF3 system models, we propose automatic support for detecting the impact of a change within system models on the assurance case model, thus enabling the integrated development of system and assurance case models.}, doi = {10.1109/ISSREW.2019.00093}, keywords = {AutoFOCUS3, model-based safety cases, ExplicitCase, Model-based systems engineering, MbSE}, } @inproceedings{kondeva19wosocer, author = {Kondeva, Antoaneta and C{\^{a}}rlan, Carmen and Rue{\ss}, Harald and Nigam, Vivek}, title = {On Computer-Aided Techniques for Supporting Safety and Security Co-Engineering}, booktitle = {Proceedings of the 2019 IEEE International Symposium on Software Reliability Engineering Workshops ({ISSREW})}, publisher = {IEEE}, year = {2019}, abstract = {With the increasing system interconnectivity, cyberattacks on safety-critical systems can lead to catastrophic events. This calls for a better safety and security integration. Indeed, a safety assessment contains security relevant information, such as, key safety hazards, that shall not be triggered by cyber-attacks. Guidelines, such as, SAE J3061 and ED202A, already recommend to exchange information gathered by safety and security engineers during different phases of development. However, these guidelines do not specify exactly how and which information shall be exchanged. We propose a methodology for enabling computer aided techniques for extracting security relevant information from safety analysis. In particular, we propose techniques for automatically constructing Attack Trees from safety artefacts such as fault trees, hazard analysis and safety patterns. Lastly, we illustrate these techniques on an Industry 4.0 application.}, doi = {10.1109/ISSREW.2019.00095}, keywords = {Model-based systems engineering, MbSE}, } @conference{, author = {Schmidmaier, Matthias and Han, Zhiwei and Weber, Thomas and Liu, Yuanting and Hu{\ss}mann, Heinrich}, title = {Real-Time Personalization in Adaptive IDEs}, booktitle = {the 27th Conference on User Modeling, Adaptation and Personalization (UMAP)}, publisher = {ACM}, pages = {81-86}, year = {2019}, owner = {Matthi}, abstract = {Integrated Development Environments (IDEs) are used for a varietyof software development tasks. Their complexity makes them chal-lenging to use though, especially for less experienced developers. In this paper, we outline our approach for an user-adaptive IDE that is able to track the interactions, recognize the user's intent and expertise, and provide relevant, personalized recommendations in real-time. To obtain a user model and provide recommendations, interaction data is processed in a two-stage process: first, we derive a bandit based global model of general task patterns from a dataset of labeled interactions. Second, when the user is working with the IDE, we apply a pre-trained classifier in real-time to get task labels from the user's interactions. With those and user feedback we fine-tune a local copy of the global model. As a result, we obtain a personalized user model which provides user-specific recommendations. We finally present various approaches for using these recommendations to adapt the IDE's interface. Modifications range from visual highlighting to task automation, including explanatory feedback.}, keywords = {Adaptive IDE; User Modeling; Personalized Recommendation Systems; Human-Centered Machine Learning}, url = {https://www.medien.ifi.lmu.de/pubdb/publications/pub/schmidmaier2019umap-lbw/schmidmaier2019umap-lbw.pdf}, } @inproceedings{evers2019roadmap, author = {Evers, Kathrin and Seyler, Jan R and Aravantinos, Vincent and L{\'{u}}cio, Levi and Mehdi, Anees}, title = {Roadmap to Skill Based Systems Engineering}, booktitle = {24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)}, publisher = {IEEE}, pages = {1093--1100}, year = {2019}, abstract = {Finding the right solution for a given automation problem is one of the biggest challenges for customers of industrial control and automation companies. This search needs to address customers’ demands and preferences such as cost-effectiveness, energy-consumption, durability, working space, etc. Consequently, solutions may comprise different products of different providers. This leads to an enormous search space of diverse potential solutions. As of today, the search process involves human effort. Thus, a good understanding of system engineering is required not only on the manufacturer side but on the customer side as well. Furthermore, integration and configuration of the products into a functional system needs extra effort.In this paper, we present our first ideas on reducing the complexity of this search task. Our approach is laid out in three layers: (i) a customer only needs to describe their desired automation application on an abstract level. (ii) manufacturers need to categorize their products as per functionality and characteristics. (iii) the linking between the requirements as per customer’s description to relevant products is done automatically.This paper provides a roadmap for the research necessary to implement these three layers in practice. We lay out the essential research questions and provide a conceptual division of the work, thus pointing out the challenges that need to be solved to allow for further automation in this area.}, doi = {10.1109/ETFA.2019.8869534}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{8719411, author = {Iqbal, Tahira and Elahidoost, Parisa and L{\'{u}}cio, Levi}, title = {A Bird's Eye View on Requirements Engineering and Machine Learning}, booktitle = {Proceedings of the 25th Asia-Pacific Software Engineering Conference (APSEC)}, pages = {11-20}, year = {2018}, month = dec, abstract = {Machine learning (ML) has demonstrated practical impact in a variety of application domains. Software engineering is a fertile domain where ML is helping in automating different tasks. In this paper, our focus is the intersection of software requirement engineering (RE) and ML. To obtain an overview of how ML is helping RE and the research trends in this area, we have surveyed a large number of research articles. We found that the impact of ML can be observed in requirement elicitation, analysis and specification, validation and management. Furthermore, in these categories, we discuss the specific problem solved by ML, the features and ML algorithms used as well as datasets, when available. We outline lessons learned and envision possible future directions for the domain.}, doi = {10.1109/APSEC.2018.00015}, keywords = {Requirements Engineering, Machine learning, State of the art, Overview, Model-based Systems Engineering, MbSE}, } @misc{, author = {L{\'{u}}cio, Levi and Voss, Sebastian and Chuprina, Tatiana and Bayha, Andreas and Eder, Johannes and Kanav, Sudeep}, title = {[T3] Develop your Own Car}, booktitle = {MODELS Conference Tutorials}, series = {MODELS 2018 Conference Tutorials, Copenhagen, Denmark}, year = {2018}, month = oct, address = {Copenhagen, Denmark}, abstract = {AutoFOCUS3 (AF3) is a mature model-driven engineering environment to develop software for embedded systems. For the past 20 years,several versions of AF3 have served as a platform for experimenting with cutting-edge research ideas in Model-Driven Development. AF3 is a tool that fully encompasses the software life cycle, from requirements, to architecture, simulation, deployment, code generation and verification. The attendees of this tutorial will be given the unique opportunity to model and deploy software on a real remote-controlled vehicle, using only AF3. Attendees will start by modeling the software controller for a blinker, which will be integrated with the model of the vehicle’s software. The generated code will then be flashed onto a Raspberry Pi contained in the physical remote-controlled model vehicle which can then be driven in the real world. Attendees who finish early will be able to model more advanced driving assistance functionalities. The last part of the tutorial will be dedicated to deepening the attendees’ understanding of the modeling capabilities of AF3 in areas such as requirements engineering, design-space exploration, building safety cases, formal verification, modeling processes, testing or variability modeling.}, keywords = {AutoFOCUS3, case study, fortissimo, rover, model-based systems engineering, MbSE}, url = {https://modelsconf2018.github.io/program/tutorials/#t3-develop-your-own-car}, } @inproceedings{, author = {Kanav, Sudeep}, title = {A modular approach to integrate verification tools in model based development}, booktitle = {Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings}, publisher = {ACM}, pages = {150--155}, year = {2018}, month = oct, abstract = {The problem of integrating an existing formal verification tool in a given software specification tool arises repeatedly both in industry and academia. At present this task is executed in an ad-hoc manner and is time consuming. Moreover, interpreting the results of the verification to locate and fix the bug (by the human user) is implicitly complicated, hence, time consuming. In this work we draft a solution for reducing the complexity of these tasks and aim at reducing the time required to complete them. We sketch a framework formalizing the concepts required to execute these tasks in a modular fashion and implement a solution based on domain specific languages (DSLs) and parameterizable model transformations. We expect that the modularity of our framework will raise its potential to be reused. We plan on evaluating this work on a set of modeling environments and a set of verification tools.}, doi = {10.1145/3270112.3275334}, keywords = {AutoFOCUS3, simulation, case study, model-based systems engineering, MbSE}, } @inproceedings{, author = {L{\'{u}}cio, Levi and Kanav, Sudeep and Bayha, Andreas and Eder, Johannes}, title = {Controlling a virtual rover using {AutoFOCUS3}}, booktitle = {Proceedings of the {MDETools} Workshop co-located with {MODELS} 2018}, series = {{CEUR} Workshop Proceedings}, volume = {2245}, pages = {356--365}, year = {2018}, month = oct, abstract = {AUTOFOCUS3 (AF3) is a mature model-driven engineering environment for developing software for embedded systems. For the past 20 years, several versions of AF3 have served as a platform for experimenting with cutting edge research ideas in Model-Driven Development. AF3 is a tool that fully encompasses the software lifecycle, from requirements, to architecture, simulation, deployment, code generation and verification. In this article, we describe how we used an existing model of a complex controller for a real-life miniature vehicle and have downsized and adapted it to control a rover in a virtual environment. The model we present here automates the maneuvering of a rover to follow an-other leader rover in a virtual environment, while keeping a safe distance to it. The controller operates by adapting the rover’s speed and steering according to the position and movements of the leader. The results we present in this article illustrate the whole development cycle of an embedded system using AF3, from the development of the model down to deployment to a specific platform as well as code generation and connecting to the hardware}, keywords = {AutoFOCUS3, case study, fortissimo, rover, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-2245/mdetools_paper_6.pdf}, } @inproceedings{eder2018exploration, author = {Eder, Johannes}, title = {Exploration of hardware topologies based on functions, variability and timing}, booktitle = {Proceedings of the 21st ACM/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings}, publisher = {ACM}, pages = {145--149}, year = {2018}, month = oct, abstract = {This paper gives an overview over a dissertation project in the area of design space exploration for distributed, embedded systems. As the engineering of distributed embedded systems is getting more and more complex due to increasingly sophisticated functionalities demanding more and more powerful hardware, automation is required in order cope with this rising complexity. Using a model based systems engineering approach enables design space exploration methods which provide such automations, given a formalization of the problem in order to be solvable e.g. by SMT solvers. In this thesis we want to provide an automated synthesis of hardware topologies (E/E architectures) based on the functions which are deployed onto this topology and constraints and optimization objectives which are derived from the requirements of the system. The synthesis shall consider variability aspects (possible variants) of the hardware elements. Additionally, timing aspects of the deployed shall be regarded such that the solution of the synthesis is a hardware topology, a deployment of functions onto this topology and a schedule of these functions. The thesis shall be evaluated by using an automotive industrial use case of realistic size.}, doi = {10.1145/3270112.3275333}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @inproceedings{eder2018deployment, author = {Eder, Johannes and Bayha, Andreas and Voss, Sebastian and Ipatiov, Alexandru and Khalil, Maged}, title = {From deployment to platform exploration: automatic synthesis of distributed automotive hardware architectures}, booktitle = {Proceedings of the 21th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems}, pages = {438--446}, year = {2018}, month = oct, organization = {ACM}, abstract = {In order to cope with the rising complexity of today's systems, model-based development of software-intensive embedded systems has become a de-facto standard in recent years. In a previous work, we demonstrated how such a model-based approach can enable automatization of certain development steps, namely the deployment of logical (platform-independent) system models to technical (platform-specific) system models. Together with Continental, we especially focused on industrial applicability. In this work, we demonstrate how we extended, again in cooperation with Continental, the previous approach in order to enable a synthesis of the topology of technical platforms (E/E architectures) together with a deployment. We furthermore introduced variability concepts in order to model variants of technical platforms which is an industrial required need. Our approach is thus capable of calculating a platform architecture and its topology which is optimized in terms of the deployment of logical system models, constraints, optimization objectives and choses the optimal variant for all technical models.}, doi = {10.1145/3239372.3239385}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE, case study}, } @inproceedings{, author = {Terzimehić, Tarik}, title = {Optimization and Reconfiguration of IEC 61499-based Software Architectures}, booktitle = {ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems (MODELS) - Doctoral Symposium}, journal = {ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems (MODELS) - Doctoral Symposium}, year = {2018}, month = oct, abstract = {The fourth industrial revolution (Industry 4.0) strives for an optimized and flexible production process to reduce configuration costs. To achieve such a production process, first architecture-level decisions (i.e. deployment configuration, scheduling, etc.) are optimized. Following, these optimized architectural configurations are applied to dynamically reconfigure industrial control applications. To calculate software configurations, current research applies Design Space Exploration (DSE) techniques embedded into the IEC 61499 model-based approach. However, this research either applies simple and non-applicable constraints and objectives for real-life problems or considers architectural optimization solely at the design phase. Thus, reconfiguring industrial control applications is still an exhausting and manual task that requires production process' downtime. In this Ph.D. thesis, I handle the automatically optimized reconfiguration of the industrial automation systems. In particular, I propose applying DSE to calculate architectural configurations of IEC 61499-based control applications. To define different configuration problems from real-world situations, I identify domain-specific constraints and objectives. Furthermore, I will tackle the problem of runtime reconfiguration by applying several optimization strategies in various context scenarios and investigating an incremental search for new optimal configurations.}, doi = {doi.org/10.1145/3270112.3275336}, keywords = {Architectural Optimization, DSE, MbSE, model-based systems engineering, Industry 4.0, IEC 61499}, } @inproceedings{, author = {Gr{\"{u}}ner, Sten and Malakuti, Somayeh and Schmitt, Johannes and Terzimehić, Tarik and Wenger, Monika and Elfham, Haitham}, title = {Alternatives for Flexible Deployment Architectures in Industrial Automation Systems}, booktitle = {23rd International Conference on Emerging Technologies And Factory Automation (ETFA)}, journal = {23rd International Conference on Emerging Technologies And Factory Automation}, year = {2018}, month = sep, abstract = {One of the main challenges of future industrial systems is to flexibly (re)deploy control applications on hardware controllers - a feature that is missing in most state of the art automation systems. Due to the heterogeneous structure of control systems, e.g. different standards and hardware, a silver bullet architecture for flexible deployment seems to be infeasible. Instead we propose an abstract architecture covering different concrete reconfiguration system architectures along with a taxonomy for design decisions for the realization of such a system. The capability of the abstract architecture is demonstrated by mapping three fundamentally different concrete reconfiguration system architectures and is verified on an industrial use case of a logistic system of an aluminum cold rolling plant.}, doi = {10.1109/ETFA.2018.8502526}, keywords = {MbSE, model-based systems engineering, deployment, reconfiguration}, } @inbook{, author = {Migge, J{\"{o}}rn and Balbastre, Patricia and Barner, Simon and Chauvel, Franck and Craciunas, Silviu S. and Diewald, Alexander and Durrieu, Guy and Haugen, Oystein and Syed, Ali Abbas Jaffari and Pagetti, Claire and Oliver, Ramon Serna and Vasilevskiy, Anatoly}, editor = {Ahmadian, Hamidreza and Obermaisser, Roman and P{\'{e}}rez, Jon}, title = {Algorithms and Tools}, booktitle = {Distributed Real-Time Architecture for Mixed-Criticality Systems}, publisher = {{CRC} Press}, pages = {98}, year = {2018}, month = aug, timestamp = 2018.08.21, abstract = {This chapter introduces the algorithms and tools to support the design and verification activities of the model driven development process. In addition, the scheduling and configuration algorithms are described to support different scheduling domains of the DREAMS architecture. This chapter begins with Section 5.1.2, which describes variability and design space exploration in the design of mixed-criticality systems. In Section 5.2, scheduling algorithms at different levels, e.g., partition level, task level, on-chip and off-chip communication are elaborated. Adaptation strategies is another topic which is covered in Section 5.3. Recovery strategies, transition modes for faster switching and algorithms for online admission of tasks in offline scheduling tables are described in this section. Timing analysis is described in Section 5.4 at different levels and Section 5.5 describes by the tools. At the Section 5.6 three toolchain use cases are presented that help to apply the toolchain.}, isbn = {978-0-8153-6064-3}, doi = {10.1201/9781351117821-5}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @inproceedings{8501293, author = {L{\'{u}}cio, Levi and Iqbal, Tahira}, title = {Formalizing EARS – First Impressions}, booktitle = {2018 1st International Workshop on Easy Approach to Requirements Syntax (EARS)}, pages = {11-13}, year = {2018}, month = aug, abstract = {The Easy Approach to Requirements Specification (EARS) has been designed primarily as a set of templates to assist requirements engineers in writing software requirements that are clear and understandable. Its target are thus requirements engineers, software architects and developers. Due to the minimalistic nature of the English sentences that make up an EARS specification, it is reasonable to expect that automated tasks can be performed on EARS specification, among which verification and code synthesis. Given English cannot be directly understood by machines without some degree of ambiguity, EARS requirements can only by automatically processed if they are translated in advance into formal specifications. In this short paper, we explore how a translation from EARS into Linear Temporal Logic can be implemented in practice.}, doi = {10.1109/EARS.2018.00009}, keywords = {EARS, Linear Temporal Logic, Translation, Formalization, Model-based Systems Engineering, MbSE}, } @inbook{, author = {Barner, Simon and Chauvel, Franck and Diewald, Alexander and Eizaguirre, Fernando and Haugen, Oystein and Migge, J{\"{o}}rn and Vasilevskiy, Anatoly}, editor = {Ahmadian, Hamidreza and Obermaisser, Roman and P{\'{e}}rez, Jon}, title = {Modeling and Development Process}, booktitle = {Distributed Real-Time Architecture for Mixed-Criticality Systems}, publisher = {{CRC} Press}, pages = {76}, year = {2018}, month = aug, timestamp = 2018.08.21, abstract = {This chapter introduces the DREAMS metamodel and a model-driven development process ranging from variability exploration to configuration synthesis. The metamodel is described in Section 4.1 and is organized into a set of viewpoints, each of which represents one system aspect. The logical viewpoint is introduced in Section 4.2 and allows for the platform-independent description of applications. The technical viewpoint enables the hierarchical description of the architecture and services of the platform. The timing viewpoint is introduced in Section 4.3 to model timing requirements that must be satisfied in order to guarantee a correct and safe operation of the system. Safety management is another topic that is covered in Section 4.4 and is supported by a safety modeling viewpoint. The deployment and resource allocation viewpoints are addressed in Section 4.5 and link the application model with the platform model. Section 4.6 describes a configuration viewpoint and defines a model-driven process to generate deployable configuration artifacts for HW/SW target platform. Lastly, in Section 4.7 a variability viewpoint constitutes the basis of a product-line exploration process.}, isbn = {978-0-8153-6064-3}, doi = {10.1201/9781351117821-4}, keywords = {AutoFOCUS3, methodology, tooling, model-based systems engineering, MbSE}, } @inproceedings{, author = {Terzimehić, Tarik and Voss, Sebastian and Wenger, Monika}, title = {Using Design Space Exploration to Calculate Deployment Configurations of IEC 61499-based Systems}, booktitle = {14th IEEE International Conference on Automation Science and Engineering (IEEE CASE 2018)}, publisher = {IEEE}, journal = {14th IEEE International Conference on Automation Science and Engineering (IEEE CASE 2018)}, year = {2018}, month = aug, abstract = {Continuous digitalization in the industry leads to new, highly complex systems that increase configuration costs. In particular, software and hardware changes cause major downtime. To dynamically reconfigure control system and avoid downtime, it is necessary to calculate valid or optimal deployment configurations. Previous research applies Design Space Exploration (DSE) techniques embedded into model-based design methodologies to calculate deployment configurations. However, current research either aims domains other than industrial automation or applies simple and, for real-life problems, not applicable constraints and objectives. Thus, the deployment of software components to hardware components is still an exhausting and manual task. In this work, we take first steps towards an automatically optimized deployment of the industrial automation systems. In particular, we propose applying DSE to calculate deployment configurations of IEC 61499-based control applications. In order to reduce the exploration space, we identify domain-specific constraints and objectives. Furthermore, we extend the IEC 61499 System and Application models' descriptions by proposing relevant hardware and software annotations. We exhibit the applicability of the identified annotations, constraints and objectives on the example of an Industry 4.0 relevant case study.}, doi = {10.1109/COASE.2018.8560591}, keywords = {IEC 61499, control system, design-space exploration, DSE, deployment, Industry 4.0, Model-based Systems Engineering, MbSE}, } @misc{, author = {Amrani, Moussa and L{\'{u}}cio, Levi and Bibal, Adrian}, title = {ML + FV = ♡? A Survey on the Application of Machine Learning to Formal Verification}, publisher = {arXiv}, number = {arXiv:1806.03600}, year = {2018}, month = jun, abstract = {Formal Verification (FV) and Machine Learning (ML) can seem incompatible due to their opposite mathematical foundations and their use in real-life problems: FV mostly relies on discrete mathematics and aims at ensuring correctness; ML often relies on probabilistic models and consists of learning patterns from training data. In this paper, we postulate that they are complementary in practice, and explore how ML helps FV in its classical approaches: static analysis, model-checking, theorem-proving, and SAT solving. We draw a landscape of the current practice and catalog some of the most prominent uses of ML inside FV tools, thus offering a new perspective on FV techniques that can help researchers and practitioners to better locate the possible synergies. We discuss lessons learned from our work, point to possible improvements and offer visions for the future of the domain in the light of the science of software and systems modeling.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://arxiv.org/abs/1806.03600}, } @inproceedings{voss2018handling, author = {Voss, Sebastian and Eder, Johannes}, title = {Handling system complexity in sCPS: usable design space exploration}, booktitle = {2018 IEEE/ACM 4th International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS)}, pages = {2--5}, year = {2018}, month = may, organization = {IEEE}, abstract = {With a growing demand for complex features in smart cyber physical systems, the design of such system is getting increasingly complex. These features demand sound and scalable approaches to deal with the increasing design space. Consequently, standards (e.g. like ISO26262) propose methods and techniques for the systematic development of (in this case: automotive) systems. The growing amount of functionality correspondingly require more powerful electronic platforms and thus methods to deal with the integration. In this paper, we describe drivers for complexity and illustrate how formal methods, namely design space exploration techniques, can be applied to deal with this complexity. This approach is based on requirements defined by the given standards and supports the system designer by a (semi-) automatic approach to handle the complexity in system design - already in early design phases.}, doi = {10.1145/3196478.3196489}, keywords = {AutoFOCUS3, design-space exploration, DSE, deployment synthesis, mapping, model-based systems engineering, MbSE}, } @inproceedings{, author = {Terzimehić, Tarik and Voss, Sebastian and Wenger, Monika and Aravantinos, Vincent}, title = {Applying DSE for Solving the Deployment Problem in Industry 4.0}, booktitle = {14th Dagstuhl Workshop on Model-Based Development of Embedded Systems (MBEES)}, publisher = {fortiss GmbH}, journal = {14th Dagstuhl Workshop on Model-Based Development of Embedded Systems (MBEES)}, year = {2018}, month = apr, keywords = {Model-based Systems Engineering, MbSE, design-space exploration, DSE}, } @inproceedings{Diewald2018, author = {Diewald, Alexander and Barner, Simon and Voss, Sebastian}, title = {Architecture Exploration for Safety-Critical Systems}, booktitle = {Proceedings of the DATE Workshop on New Platforms for Future Cars: Current and Emerging Trends (NPCAR)}, year = {2018}, month = mar, abstract = {Future cars will host massively more functionality that comes along with the introduction of new technologies such as neural networks and data fusion, which are enablers for autonomous driving, but which require massive processing capabilities. Hence, new architectures are required that can handle the contradicting requirements for efficiency and safety compliance. The increased complexity and size of upcoming target architectures raise the need for advanced design methodologies and tool support. In this work, we present an approach that combines model-driven development (MDD) with design space exploration (DSE) that can explore suitable architectures of safety functions and platforms also in early design phases and enables trade-off decisions. The DSE uses optimization decomposition for complexity reduction and reusability while respecting the dependencies implied by development processes.}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @article{, author = {Becker, Klaus and Voss, Sebastian and Sch{\"{a}}tz, Bernhard}, title = {Formal analysis of feature degradation in fault-tolerant automotive systems}, journal = {Science of Computer Programming}, volume = {154}, number = {1}, pages = {89--133}, year = {2018}, month = mar, abstract = {Safety critical fault-tolerant embedded systems have to react properly on failures of internal system elements to avoid failure propagation and finally a harmful external failure at the system boundary. Beside failure detection, actions for failure handling are essential to cover safety requirements. Actions reach from enabling fail-silent, fail-safe or fail-operational behavior of system elements, or also hybrids of this in a mixed criticality system design. Graceful degradation can be applied when system resources become insufficient, reducing the set of provided functional features. In this paper, we address mixed criticality and mixed reliability automotive systems. We consider mixed reliability by functional features having different fail-operational requirements. Beside pure fail-operational features, we also consider degradations of functional features, called fail-degraded features. We describe a formal system model that contains, i.a., the functional features of a vehicle, possible feature degradations, software components that realize the features, as well as the deployment of software components to execution units. We provide a structural analysis of the level of degradation on system level and feature level, which is required in scenarios of failing execution units and/or software components. Combined with this analysis, we synthesize valid deployments of software components to execution units, incorporating an adequate level of redundancy to meet the fail-operational requirements, if feasible. We apply our approach to a constructed automotive example.}, doi = {10.1016/j.scico.2017.10.007}, keywords = {Graceful degradation, Fault tolerance, Redundancy, Fail-operational, Mixed criticality, Model-based Systems Engineering, MbSE}, } @inproceedings{SchneiderMaMo2018, author = {Schneider, Ben and Voss, Sebastian and Wenger, Monika and Zoitl, Alois}, title = {Using IEC 61499 Models for Automatic Network Configuration of Distributed Automation Systems}, booktitle = {9th Vienna International Conference on Mathmatical Modelling (MATHMOD2018)}, year = {2018}, month = feb, timestamp = 2018.02.21, abstract = {The new Ethernet standard Time-Sensitive Networking is an enabler for Industrial Internet of Things (IIoT) but gets more and more difficult to configure with a continuous rising number of network nodes, because each node has to be set up separately. We propose an approach towards automatic configuration of real-time networks based on models of IEC 61499, a modeling language for distributed industrial automation systems. Therefore, these existing models are analysed w.r.t. their network modeling capabilities and missing information is shown.}, keywords = {distributed industrial automation, IEC 61499, Time-Sensitive Networking, TSN, real-time, deterministic networking, schedule synthesis, model-based systems engineering, MbSE}, language = {english}, } @inproceedings{DBLP:conf/fmcad/LeonFHM18, author = {Ponce de Le{\'{o}}n, Hern{\'{a}}n and Furbach, Florian and Heljanko, Keijo and Meyer, Roland}, title = {{BMC} with Memory Models as Modules}, booktitle = {{FMCAD}}, publisher = {{IEEE}}, pages = {1--9}, year = {2018}, abstract = {This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach.}, doi = {10.23919/FMCAD.2018.8603021}, keywords = {Model-based Systems Engineering, MbSE}, } @article{DBLP:journals/fmsd/LeonM18, author = {Ponce de Le{\'{o}}n, Hern{\'{a}}n and Mokhov, Andrey}, title = {Compact and efficiently verifiable models for concurrent systems}, journal = {Formal Methods in System Design}, volume = {53}, pages = {407--431}, year = {2018}, abstract = {Partial orders are a fundamental mathematical structure capable of representing concurrency and causality on a set of atomic events. In many applications it is essential to consider multiple partial orders, each representing a particular behavioral scenario or an operating mode of a system. With the exploding growth of the complexity of systems that software and hardware engineers design today, it is no longer feasible to represent each partial order of a large system explicitly, therefore compressed representations of sets of partial orders become essential for improving the scalability of design automation tools. In this paper we study two well known mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures and Conditional Partial Order Graphs. We discuss their advantages and disadvantages and propose efficient algorithms for transforming a set of partial orders from a given compressed representation in one formalism into an equivalent representation in another formalism without explicitly enumerating every partial order. The proposed algorithms make use of an intermediate mathematical formalism which we call Conditional Labeled Event Structures that combines the advantages of both structures. Finally, we compare these structures on a number of benchmarks coming from concurrent software and hardware domains.}, doi = {10.1007/s10703-018-0316-0}, keywords = {Model-based Systems Engineering, MbSE}, } @article{, author = {Oakes, Bentley James and Troya, Javier and L{\'{u}}cio, Levi and Wimmer, Manuel}, title = {Full contract verification for ATL using symbolic execution}, journal = {Software & Systems Modeling}, volume = {17}, pages = {815--849}, year = {2018}, abstract = {The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time.}, doi = {10.1007/s10270-016-0548-7}, keywords = {Model transformation, ATL, Formal verification, Symbolic execution, Contracts, Pre-/post-conditions, Model-based Systems Engineering, MbSE}, } @article{DBLP:journals/isci/LeonNCB18, author = {Ponce de Le{\'{o}}n, Hern{\'{a}}n and Nardelli, Lucio and Carmona Josep, and K. L. M. vanden Broucke, Seppe}, title = {Incorporating negative information to process discovery of complex systems}, journal = {Inf. Sci.}, volume = {422}, pages = {480--496}, year = {2018}, abstract = {The discovery of a formal process model from event logs describing real process executions is a challenging problem that has been studied from several angles. Most of the contributions consider the extraction of a model as a one-class supervised learning problem where only a set of process instances is available. Moreover, the majority of techniques cannot generate complex models, a crucial feature in some areas like manufacturing. In this paper we present a fresh look at process discovery where undesired process behaviors can also be taken into account. This feature may be crucial for deriving process models which are less complex, fitting and precise, but also good on generalizing the right behavior underlying an event log. The technique is based on the theory of convex polyhedra and satisfiability modulo theory (SMT) and can be combined with other process discovery approach as a post processing step to further simplify complex models. We show in detail how to apply the proposed technique in combination with a recent method that uses numerical abstract domains. Experiments performed in a new prototype implementation show the effectiveness of the technique and the ability to be combined with other discovery techniques.}, doi = {10.1016/j.ins.2017.09.027}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Huber, Michael M. and Brunner, Michael and Sauerwein, Clemens and C{\^{a}}rlan, Carmen and Breu, Ruth}, title = {Roadblocks on the Highway to Secure Cars: An Exploratory Survey on the Current Safety and Security Practice of the Automotive Industry}, booktitle = {Proceedings of the 37th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2018)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11093}, pages = {157--171}, year = {2018}, abstract = {With various advances in technology, cars evolved to highly interconnected and complex Cyber-Physical Systems. Due to this development, the security of involved components and systems needs to be addressed in a rigorous way. The resulting necessity of combining safety and security aspects during the development processes has proven to be non-trivial due to the high interference between these aspects and their respective treatment. This paper discusses the results of an exploratory survey on how organizations from the automotive industry in the Euroregion tackle the challenge of integrating safety and security aspects during system development. The observed state of practice shows that there are significant deficits in the integration of both domains. The results of the exploratory survey enabled us to identify the most common challenges of realizing an integrated approach in a practical setting and discuss implications for future research.}, doi = {10.1007/978-3-319-99130-6_11}, keywords = {Automotive, Cyber-Physical Systems, Safety-Security Integration, Industrial survey, Model-based systems engineering, MbSE}, } @inproceedings{eder2017bringing, author = {Eder, Johannes and Zverlov, Sergey and Voss, Sebastian and Khalil, Maged and Ipatiov, Alexandru}, title = {Bringing DSE to life: exploring the design space of an industrial automotive use case}, booktitle = {2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, pages = {270--280}, year = {2017}, month = sep, organization = {IEEE}, abstract = {In order to cope with the rising complexity of today's systems, model-based development of software-intensive embedded systems has become a de-facto standard in recent years. Such a development approach enables a variety of frontloading methods. Design space exploration is one of those techniques. However, in order to properly perform a valid exploration, a system model has to have a certain quality. This requires dedicated, meaningful models as an input according to well-known design principles, which entails the structuring of models according to different viewpoints and usage of dedicated models for each of these viewpoints.In this work, we demonstrate how, based on an industrial application model represented in SysML, design space exploration methods can be efficiently applied to enable the synthesis of deployments from a logical (platform-independent) system models to technical (platform-specific) system models. Moreover, we will demonstrate the applicability of this approach by a project conducted with Continental.}, doi = {10.1109/MODELS.2017.36}, keywords = {AutoFOCUS3, design-space exploration, DSE, deployment synthesis, mapping, model-based systems engineering, MbSE, case study}, } @inproceedings{, author = {Barner, Simon and Diewald, Alexander and Migge, J{\"{o}}rn and Syed, Ali Abbas Jaffari and Fohler, Gerhard and Faug{\`{e}}re, Madeleine and Gracia P{\'{e}}rez, Daniel}, title = {DREAMS Toolchain: Model-Driven Engineering of Mixed-Criticality Systems}, booktitle = {Proceedings of the ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS '17)}, publisher = {IEEE}, pages = {259--269}, year = {2017}, month = sep, abstract = {Mixed-criticality systems (MCS) aim at boosting the integration density in safety-critical systems, resulting into efficient systems, while simultaneously providing increased performance. The DREAMS project provides a cross-domain architectural style for MCS based on networked, virtualized multi-cores controlled by hierarchical resource managers. However, the availability of a platform is only one side of the coin: deploying mixed-critical applications to shared resources typically requires design-time configurations (e.g., to ensure real-time constraints or separation constraints mandated by safety regulations). These configurations are the outcome of complex optimization problems which are intractable in a manual process that also hardly can guarantee the consistency of all deployable artefacts nor their traceability to the requirements. However, existing toolchains lack support for MCS integration, and particularly DREAMS' advanced platform capabilities. We present an integrated model-driven toolchain and the underlying metamodels covering all relevant aspects of MCS including applications, timing, platforms, deployments, configurations and annotations for extra-functional properties such as safety. The approach focuses on the left branch of the V-cycle, and ranges from product-line and design space exploration to resource allocation and configuration generation. We report on the integration of exploration tools and a reconfiguration graph synthesizer, and evaluate the resulting toolchains in two use cases consisting of a product-line of wind power control applications and an avionic subsystem respectively.}, doi = {10.1109/MODELS.2017.28}, keywords = {Multicore processing, Resource management, Safety, Tools, Mixed-Criticalitity Systems, , Product-Lines, AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @inproceedings{LeviEARSCTRL2017, author = {L{\'{u}}cio, Levi and Rahman, Salman and bin Abid, Saad and Mavin, Alistair}, title = {EARS-CTRL: Building and Verifying Controllers for Dummies}, booktitle = {Tools and Demo Session track at MoDELS 2017}, pages = {1--6}, year = {2017}, month = sep, location = {Austin, Taxes}, abstract = {In this paper we present the EARS-CTRL tool forsynthesizing and validating controller software for embeddedsystems. EARS-CTRL has as starting point requirements writtenin (English) natural language, more specifically in the EARS(Easy Approach to Requirements Syntax) language invented atRolls-Royce and currently in use at numerous organizationsaround the world. After expressing the requirements in English,the requirements engineer can produce the controller code atthe press of a button. EARS-CTRL then provides facilitiesfor validating the generated controller that allow step-by-stepsimulation or test-case generation using MATLAB Simulink.}, keywords = {Software Controllers, Natural Language, Code Synthesis, MatLab Simulink, Model-based Systems Engineering, MbSE}, url = {http://ceur-ws.org/Vol-2019/demos_2.pdf}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Barner, Simon and Diewald, Alexander and Tsalidis, Alexandros and Voss, Sebastian}, title = {ExplicitCase: Integrated Model-based Development of System and Safety Cases}, booktitle = {Proceedings of the SAFECOMP 2017 Workshops ASSURE, DECSoS, SASSUR, TELERISE, and TIPS}, publisher = {Springer}, series = {LNCS}, volume = {10489}, pages = {52 -- 63}, year = {2017}, month = sep, timestamp = 2017.09.12, abstract = {Tools for creating safety cases currently on the market target safety experts, whose main concern is the management of safety cases. However, for safety assurance, safety experts should collaborate with technical experts, who have better understanding of technical and operational hazards. Thus, there should be a closer collaboration between the management of safety cases and technical expertise. Technical expertise may be retrieved, among others, from model-based system artifacts and processes. In order to close the gap between safety and technical expertise, we present ExplicitCase, an open-source tool for semi-automatic modeling, maintenance, and verification of safety cases integrated with system models. The advantage of this tool is two-fold. First, it enables its users to capture safety relevant information from model-based artifacts into safety cases. Second, it makes the safety cases rationale available to engineers in order to help them reason about design choices, while minding safety concerns. We evaluate the approach and the implemented tool based on the experiences obtained in a project use case.}, isbn = {978-3-319-66284-8}, doi = {10.1007/978-3-319-66284-8_5}, keywords = {Safety Cases, Goal Structuring Notation, System Models, AutoFOCUS3, model-based safety cases, ExplicitCase, model-based systems engineering, MbSE}, } @techreport{, author = {Oakes, Bentley James and L{\'{u}}cio, Levi and Gomes, Cl{\'{a}}udio and Vangheluwe, Hans}, title = {Expressive Symbolic-Execution Contract Proving for the {DSLTrans} Transformation Language}, publisher = {McGill University, School of Computer Science}, number = {2017-01}, year = {2017}, month = sep, school = {McGill University, School of Computer Science}, abstract = {The verification of model transformations is key for the adoption of model-driven engineering in academic and industrial processes. In this work, we provide a verification technique for our model transformation language DSLTrans, which is both confluent and terminating by construction. This technique proves structural pre-condition/ post-condition structural contracts for all inputs to a transformation. This is achieved by creating path conditions for the transformation through a symbolic execution of the transformation’s rules. These path conditions then represent all possible transformation executions through an abstraction relation. In this work, we provide a detailed description of both the path condition construction and contract proving techniques. As well, we provide arguments that our techniques are valid, such that proving a contract on the finite set of path conditions for a transformation implies that the contract holds on the infinite set of abstracted transformation executions.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://www.cs.mcgill.ca/media/tech_reports/None_Expressive_Symbolic-Execution_Contract_Proving_for_the_DSLTrans_Transf_Lky5uCT.pdf}, } @inproceedings{, author = {Nicolas, Carlos-Fernando and Eizaguirre, Fernando and Ortube, Asier Larrucea and Barner, Simon and Chauvel, Franck and Sagardui, Goiuria and P{\'{e}}rez, Jon}, title = {GSN Support of Mixed-Criticality Systems Certification}, booktitle = {Proceedings of the SAFECOMP 2017 Workshops ASSURE, DECSoS, SASSUR, TELERISE, and TIPS}, publisher = {Springer}, series = {LNCS}, number = {10489}, pages = {157--172}, year = {2017}, month = sep, timestamp = 2017.09.12, abstract = {Safety-critical applications could benefit from the standardisation, cost reduction and cross-domain suitability of current heterogeneous computing platforms. They are of particular interest for Mixed-Criticality Product Lines (MCPL) where safety- and non-safety functions can be deployed on a single embedded device using suitable isolation artefacts and development processes. The development of MCPLs can be facilitated by providing a reference architecture, a model-based design, analysis tools and Modular Safety Cases (MSC) to support the safety claims. In this paper, we present a method based on the MSCs to ease the certification of MCPLs. This approach consists of a semi-automated composition of layered argument fragments that trace the safety requirements argumentation to the supporting evidences. The core of the method presented in this paper is an argument database that is represented using the Goal Structuring Notation language (GSN). The defined method enables the concurrent generation of the arguments and the compilation of evidences, as well as the automated composition of safety cases for the variants of products. In addition, this paper exposes an industrial-grade case study consisting of a safety wind turbine system where the presented methodology is exemplified.}, isbn = {978-3-319-66284-8}, doi = {10.1007/978-3-319-66284-8_14}, keywords = {Goal Structuring Notation (GSN), Model-Based Development, Safety-critical Systems, Product Lines, Variability}, } @inproceedings{LucioProcess2017, author = {L{\'{u}}cio, Levi and bin Abid, Saad and Rahman, Salman and Aravantinos, Vincent and Harwardt, Eduard and Kuestner, Ralf}, title = {Process-Aware Model-Driven Development Environments}, booktitle = {MODELS Workshops}, pages = {405--411}, year = {2017}, month = sep, abstract = {Due to recent advances in Domain Specific Language (DSL) workbenches, it has become possible to build model-driven development environments as sets of individual DSLs that get composed for a specific purpose. In this paper we explore how model-driven development environments can become process-aware, to assist the user when building a model. We offer an explanation to our ideas at three levels of abstraction: 1) the meta-meta level, the Meta-Programming System (MPS) workbench with its language definition capabilities; 2) the meta level, where brick DSLs are defined and assembled into frameworks that are further tailored for particular modelling scenarios through the introduction of an explicit process for model construction; and 3)the model level, where models are built through progressive tool-guided refinements and automated steps based on the process introduced at the metalevel. We exemplify our approach by providing the main highlights of the ongoing development of a model-driven requirements gathering environment for our industrial partners.}, keywords = {Process-awareness, Domain-Specific Languages, DSLs, Model Construction, generic requirement gathering, framework, process language, requirement refinement process, requirement engineer, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-2019/flexmde_4.pdf}, } @phdthesis{, author = {Becker, Klaus}, title = {Software Deployment Analysis for Mixed Reliability Automotive Systems}, publisher = {TU M{\"{u}}nchen}, year = {2017}, month = jun, organization = {TU M{\"{u}}nchen}, school = {TU M{\"{u}}nchen}, institution = {TU M{\"{u}}nchen}, abstract = {Safety critical systems require rising dependability due to increasing autonomy. Fault-tolerance is necessary, but failures may cause system resources to become insufficient to provide all intended functional features. We introduce an approach to formally analyze failure scenarios in mixed criticality systems, combined with the synthesis of valid deployments of software to hardware, incorporating adequate redundancy to address mixed reliability. Based on a formal system model, we provide a structural analysis of necessary degradations and failovers in failure scenarios, while ensuring the fulfillment of fail-operational requirements.}, keywords = {Fault Tolerance, Graceful Degradation, Fail-Operational, Dependability, Reliability, Mixed Criticality, Safety, Deployment, Redundancy, Synthesis, Automotive, Formal Methods, Model-based Systems Engineering, MbSE}, url = {http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20170726-1345914-1-1}, } @inproceedings{, author = {L{\'{u}}cio, Levi and Rahman, Salman and Cheng, Chih-Hong and Mavin, Alistair}, title = {Just Formal Enough? Automated Analysis of {EARS} Requirements}, booktitle = {NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings}, pages = {427--434}, year = {2017}, month = may, abstract = {EARS is a technique used by Rolls-Royce and many other organizations around the world to capture requirements in natural language in a precise manner. In this paper we describe the EARS-CTRL tool for writing and analyzing EARS requirements for controllers. We provide two levels of analysis of requirements written in EARS-CTRL: firstly our editor uses projectional editing as well as typing (based on a glossary of controller terms) to ensure as far as possible well-formedness by construction of the requirements; secondly we have used a controller synthesis tool to check whether a set of EARS-CTRL requirements is realizable as an actual controller. In the positive case, the tool synthesizes and displays the controller as a synchronous dataflow diagram. This information can be used to examine the specified behavior and to iteratively correct, improve or complete a set of EARS-CTRL requirements.}, doi = {10.1007/978-3-319-57288-8_31}, keywords = {Natural Language, Linear Temporal Logic, Requirement Engineer, Controller Synthesis, Model-based Systems Engineering, MbSE}, url = {https://doi.org/10.1007/978-3-319-57288-8\_31}, crossref = {DBLP:conf/nfm/2017}, } @phdthesis{, author = {Teufl, Sabine}, title = {Seamless Model-based Requirements Engineering: Models, Guidelines, Tools}, year = {2017}, month = may, school = {Technische Universit{\"{a}}t M{\"{u}}nchen}, abstract = {A practical model-based approach for requirements engineering (RE) should address all of the following challenges: Textual documentation; analysis, validation and verification of requirements; the integration of RE into a comprehensive development approach; guidance and tool support. These challenges have previously been studied in isolation. This work examines these challenges holisticly, selects models, guidelines and tool support, and integrates them into a seamless model-based RE approach.}, type = {Dissertation}, keywords = {AutoFOCUS3, MIRA, model-based requirements engineering, model-based systems engineering, MbSE}, url = {http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20171006-1360281-1-5}, } @inproceedings{, author = {Gleirscher, Mario and C{\^{a}}rlan, Carmen}, title = {Arguing from Hazard Analysis in Safety Cases: A Modular Argument Pattern}, booktitle = {2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE)}, publisher = {IEEE}, pages = {53--60}, year = {2017}, abstract = {We observed that safety arguments are prone tostay too abstract, e.g. solutions refer to large packages, argumentstrategies to complex reasoning steps, contexts and assumptionslack traceability. These issues can reduce the confidence werequire of such arguments. In this paper, we investigate theconstruction of confident arguments from (i) hazard analysis(HA) results and (ii) the design of safety measures, i.e., bothused for confidence evaluation. We present an argument patternintegrating three HA techniques, i.e., FTA, FMEA, and STPA, aswell as the reactions on the results of these analyses, i.e., safetyrequirements and design increments. We provide an example ofhow our pattern can help in argument construction and discusssteps towards using our pattern in formal analysis and computer-assisted construction of safety cases.}, doi = {10.1109/HASE.2017.15}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{2017_carlan_appropriateness, author = {C{\^{a}}rlan, Carmen and Gallina, Barbara and Kacianka, Severin and Breu, Ruth}, title = {Arguing on Software-Level Verification Techniques Appropriateness}, booktitle = {Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP)}, publisher = {Springer International Publishing}, series = {LNCS}, volume = {10488}, pages = {39--54}, year = {2017}, address = {Cham}, abstract = {In this paper, we investigate the pondered selection of innovative software verification technology in the safety-critical domain and its implications. Verification tools perform analyses, testing or simulation activities. The compliance of the techniques implemented by these tools to fulfill standard-mandated objectives (i.e., to be means of compliance in the context of DO-178C and related supplements) should be explained to the certification body. It is thereby difficult for practitioners to use novel techniques, without a systematic method for arguing their appropriateness. Thus, we offer a method for arguing the appropriate application of a certain verification technique (potentially in combination with other techniques) to produce the evidence needed to satisfy certification objectives regarding fault detection and mitigation in a realistic avionics application via safety cases. We use this method for the choice of an appropriate compiler to support the development of a drone.}, isbn = {978-3-319-66266-4}, doi = {10.1007/978-3-319-66266-4_3}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen}, title = {Living Safety Arguments for Open Systems}, booktitle = {Proceedings of the 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)}, publisher = {IEEE}, year = {2017}, abstract = {In recent years, there has been a shift from closed systems, with clearly defined borders, whose behavior is completely determined a priori, towards open systems. An open system is an independently developed system, which is able to communicate and cooperate with other open systems in an ad-hoc manner, at runtime. Moreover, due to their openness, such systems may be used in various contexts. Whenever open systems collaborate in a safety-critical context at runtime, the functional safety of both the individual open systems and emerged system of open systems needs to be assured. More and more regulations nowadays require a safety argumentation of the system. I thereby propose an approach for automatically adapting the safety argumentation built manually, during design time, according to the new operational environment information. To evaluate and validate the proposed solution, the approach will be applied to 1) a system of autonomous drones cooperating for intelligent intersection management, and 2) a system of cooperative transport robots in an industrial setting.}, doi = {10.1109/ISSREW.2017.58}, keywords = {Model-based Systems Engineering, MbSE}, } @article{DBLP:journals/tecs/SaarikiviLKHE17, author = {Saarikivi, Olli and Ponce de Le{\'{o}}n, Hern{\'{a}}n and K{\"{a}}hk{\"{o}}nen, Kari and Heljanko, Keijo and Esparza, Javier}, title = {Minimizing Test Suites with Unfoldings of Multithreaded Programs}, journal = {ACM Trans. Embedded Comput. Syst.}, volume = {16}, number = {2}, pages = {45:1--45:24}, year = {2017}, abstract = {This article focuses on computing minimal test suites for multithreaded programs. Based on previous work on test case generation for multithreaded programs using unfoldings, this article shows how this unfolding can be used to generate minimal test suites covering all local states of the program. Generating such minimal test suites is shown to be NP-complete in the size of the unfolding. We propose an SMT encoding for this problem and two methods based on heuristics which only approximate the solution, but scale better in practice. Finally, we apply our methods to compute the minimal test suites for several benchmarks.}, doi = {10.1145/3012281}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{DBLP:conf/models/KanavA17, author = {Kanav, Sudeep and Aravantinos, Vincent}, title = {Modular Transformation from {AF3} to nuXmv}, booktitle = {Proceedings of {MODELS} 2017 Satellite Event: Workshops (ModComp, ME, EXE, COMMitMDE, MRT, MULTI, GEMOC, MoDeVVa, MDETools, FlexMDE, MDEbug), Posters, Doctoral Symposium, Educator Symposium, {ACM} Student Research Competition, and Tools and Demonstrations}, pages = {300--306}, year = {2017}, abstract = {{AutoFOCUS3 (AF3)} supports formal verification of its models using the {nuXmv} model checker. This requires a model transformation from {AF3} to {nuXmv} models. In this paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community.}, keywords = {AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-2019/modevva_1.pdf}, crossref = {DBLP:conf/models/2017s}, } @inproceedings{DBLP:conf/sas/LeonFHM17, author = {Ponce de Le{\'{o}}n, Hern{\'{a}}n and Furbach, Florian and Heljanko, Keijo and Meyer, Roland}, title = {Portability Analysis for Weak Memory Models. {PORTHOS:} One Tool for all Models}, booktitle = {{SAS}}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {10422}, pages = {299--320}, year = {2017}, abstract = {We present PORTHOS, the first tool that discovers porting bugs in performance-critical code. PORTHOS takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, PORTHOS finds a bug in the form of an unexpected execution}, doi = {10.1007/978-3-319-66706-5\_15}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://doi.org/10.1007/978-3-319-66706-5\_15}, } @inproceedings{8101258, author = {Aravantinos, Vincent and Kanav, Sudeep}, title = {Tool Support for Live Formal Verification}, booktitle = {2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, pages = {145-155}, year = {2017}, abstract = {Despite an increasing interest from industry (e.g., DO333 standard [1]), formal verification is still not widely used in production for safety critical systems. This has been recognized for a while and various causes have been identified, one of them being the lack for scalable and cost effective tools. Many such tools exist for formal verification, but few of them are userfriendly: using formal verification generally still requires such an effort that the time spent on the tool prevents the integration of the method in an industrial setting. This paper presents a tool prototype aiming at supporting non-experts in using formal verification. The tooling approach is meant to be cost effective and change-supportive: user-friendliness is designed not only for the non-expert, but also to require minimum effort so that formal verification is triggered even for the non-enthusiast who is not willing to push a button. To do so, we trigger, in a background task, pre-defined formal verification checks at (almost) every change of the model. We only display error messages in case of problem: the user is not disturbed if no problem is detected. To prevent checks to be triggered all the time, we decide to consider only local analyses (i.e., only checks which do not require knowledge of elements in a remote position in the model). This restricts the sort of formal verification that we support, but this is a conscious choice: our motto is ”Let us first make basic techniques very user-friendly; more powerful ones will be considered only when at least the basic techniques have proven to be accepted”.}, doi = {10.1109/MODELS.2017.6}, keywords = {program verification, software tools, formal verification, safety critical systems, automata, component architectures, AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, } @article{Kross:2017a, author = {Kro{\ss}, Johannes and Voss, Sebastian and Krcmar, Helmut}, title = {Towards a Model-driven Performance Prediction Approach for Internet of Things Architectures}, publisher = {RonPub}, journal = {Open Journal of Internet Of Things}, series = {OJIOT}, volume = {3}, number = {1}, pages = {136-141}, year = {2017}, abstract = {Indisputable, security and interoperability play major concerns in Internet of Things (IoT) architectures and applications. In this paper, however, we emphasize the role and importance of performance and scalability as additional, crucial aspects in planning and building sustainable IoT solutions. IoT architectures are complicated system-of-systems that include different developer roles, development processes, organizational units, and a multilateral governance. Its performance is often neglected during development but becomes a major concern at the end of development and results in supplemental efforts, costs, and refactoring. It should not be relied on linearly scaling for such systems only by using up-to-date technologies that may promote such behavior. Furthermore, different security or interoperability choices also have a considerable impact on performance and may result in unforeseen trade-offs. Therefore, we propose and pursue the vision of a model-driven approach to predict and evaluate the performance of IoT architectures early in the system lifecylce in order to guarantee efficient and scalable systems reaching from sensors to business applications.}, issn = {2364-7108}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://www.ronpub.com/OJIOT_2017v3i1n12_Kross.pdf}, } @inproceedings{, author = {Terzimehić, Tarik and Wenger, Monika and Zoitl, Alois and Bayha, Andreas and Becker, Klaus and M{\"{u}}ller, Thorsten and Schauerte, Hubertus}, title = {Towards an Industry 4.0 Compliant Control Software Architecture Using IEC 61499 & OPC UA}, booktitle = {IEEE International Conference on Emerging Technologies And Factory Automation (ETFA)}, year = {2017}, abstract = {The fourth industrial revolution introduced additional requirements on the industrial systems' control software in order to cope with current manufacturing systems' flexibility demands. These requirements include, among others, a dynamic reconfigurability, software reusability and an external service orchestration. This work presents the design of an industry 4.0 compliant control software architecture resulting from an iterative design process. The architecture is based on the reconfiguration services of the IEC 61499 standard and the service orchestration via OPC UA. We demonstrate the software architecture's compliance to the industry 4.0 requirements on an aluminum cold rolling mill plant demonstrator.}, doi = {10.1109/ETFA.2017.8247718}, keywords = {Industry 4.0, MbSE, model-based systems engineering, OPC UA, IEC 61499}, } @inproceedings{, author = {Zverlov, Sergey}, title = {Decomposition of Design Space Exploration Problems in the Context of model-based Development}, booktitle = {Proceedings of the Doctoral Symposium at the 19th ACM/IEEE International Conference of Model-Driven Engineering Languages and Systems ({MODELS} 2016)}, publisher = {{CEUR}}, year = {2016}, month = oct, abstract = {During the development process of complex embedded systems there typically is a large number of architectural decisions that engineers are facing. Each of them can influence the properties of the end result (ie: cost, performance, etc.). A systematic process that supports this decision making is often referred to as Design Space Exploration (DSE). The need for computer-aided DSE methods was recognized by the research community which resulted in a large number of publications in this area. The contribution of this PhD project is two-fold: First contribution is a classification of typical DSE problems that arise during the development process of embedded systems. Due their high popularity in this area the focus of this work lies on the model-based approaches. The second contribution is two provide a decomposition approach for complex DSE problems. The decomposition strategy is thereby based on the previously identified DSE problem classes.}, keywords = {Design Space Exploration, Model-Based Systems Engineering, MbSE, Decomposition, Architecture Optimization}, url = {http://ceur-ws.org/Vol-1735/paper3.pdf}, } @inproceedings{, author = {Eder, Johannes and Voss, Sebastian}, title = {Usable Design Space Exploration in {AutoFOCUS3}}, booktitle = {Joint Proceedings of the 12th Educators Symposium (EduSymp 2016) and 3rd International Workshop on Open Source Software for Model Driven Engineering (OSS4MDE 2016) co-located with MODELS 2016}, publisher = {CEUR-WS}, pages = {51--58}, year = {2016}, month = oct, abstract = {Software-intensive embedded systems are characterized by an increasing number of features that implement complex functionalities. To effectively manage this complexity, development processes in general, and model-based approaches in particular, support the development of such systems as model-based approaches have been considered a central design approach to deal with increasing complexity in software and hardware development. A valid system design and configuration, especially a safety-critical system design, has to fulfill a corresponding set of requirements describing all desired system constraints and objectives. In general, these constraints may be contradicting and correspond to different dimensions (e.g. timing, safety, energy, cost, etc.). Thus, considering all system constraints during system design is a manually unsolvable task. To support the system designer, usable Design Space Exploration methods are needed. Therefore, a proper tool implementation is needed that supports the usability. In this paper, we describe a Design Space Exploration process which aims to explore the architectural design space during system design. This process has been implemented in the open source CASE tool AutoFOCUS3 with the focus on usability.}, keywords = {AutoFOCUS3, design-space exploration, DSE, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-1835/paper08.pdf}, } @inproceedings{Barner2016, author = {Barner, Simon and Diewald, Alexander and Eizaguirre, Fernando and Vasilevskiy, Anatoly and Chauvel, Franck}, title = {Building Product-lines of Mixed-Criticality Systems}, booktitle = {Proceedings of the Forum on Specification and Design Languages (FDL 2016)}, publisher = {IEEE}, year = {2016}, month = sep, address = {Bremen, Germany}, abstract = {Mixed-Criticality Systems (MCS) reconcile safety-critical requirements with multi-core architectures, by offering spatial and temporal isolation while preserving other extra-functional properties such as optimised energy consumption or minimised latencies. MCS designers struggle to manually balance the offered functionalities with pertinent implementation choices in order to ensure that the system eventually meets all constraints. Existing attempts to further automate this process focus on specific concerns, and fail to account for variation in system functionalities. Our contribution is to integrate product-lines that capture functional variations with evolutionary optimisation to explore possible implementations and their impact on extra-functional properties. Our solution is a model-driven process (and a tool prototype) to automatically select functionally different products that balance well the various concerns of interest. We illustrate how this process applies to the construction of wind turbines.}, doi = {10.1109/FDL.2016.7880378}, keywords = {Product-lines, cyber-physical systems, MCS, evolutionary optimisation, mixed-criticality systems, multicore architectures, wind turbines, Energy consumption, AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @inproceedings{voss2016schedule, author = {Voss, Sebastian and Eder, Johannes and Sch{\"{a}}tz, Bernhard}, title = {Schedule synthesis for multi-period SW components}, booktitle = {SAE 2016 World Congress and Exhibition}, publisher = {SAE International}, year = {2016}, month = apr, institution = {SAE Technical Paper}, abstract = {The growing complexity of functionalities in automotive vehicles and their safety-criticality, including timing requirements, demands sound and scalable approaches to deal with the increasing design space. Most often, such complex automotive systems are composed of a set of functions that are characterized by multi-period timing behaviors, e.g., due to environment constraints limiting sensing/acting frequencies, or various worst case execution times of software components.As safety-critical systems must perform the desired behavior within guaranteed time bounds, a valid system configuration is needed including a time-correct schedule that fulfills all timing requirements. This contribution proposes a systematic and correct schedule synthesis of complex multi-rate automotive software systems that ensures precise timing behavior of software components.The proposed synthesis approach - guaranteeing given timing requirements, based on preemptive, time-triggered scheduling - optimizes non-harmonic task sets by minimizing context switches between these tasks. This approach is integrated into the AUTOFOCUS 3 tool-chain, using its models of a software component architecture as well as of a hardware platform, combined with precalculated interrupt sets and a symbolic encoding scheme to synthesize schedules meeting the given multi-rate timing requirements. The approach is demonstrated using an Adaptive Cruise Control System.}, issn = {2688-3627}, doi = {10.4271/2016-01-0012}, keywords = {AutoFOCUS3, design-space exploration, DSE, scheduling, model-based systems engineering, MbSE}, } @inproceedings{Prehofer:TTApfoC:2016, author = {Prehofer, Christian and Horst, Oliver and Dodi, Riccardo and Geven, Arjan and Kornaros, George and Montanari, Eleonora and Paolino, Michele}, title = {Towards Trusted Apps platforms for open {CPS}}, booktitle = {3rd International Workshop on Emerging Ideas and Trends in Engineering of Cyber-Physical Systems {(EITEC)}}, pages = {23--28}, year = {2016}, month = apr, owner = {horst}, abstract = {For many cyber-physical systems, there is a strong trend towards open systems, which can be extended during operation by instantly adding functionalities on demand. We discuss this trend in the context of automotive and medical systems. The goal of this paper is to elaborate the research challenges of new platforms for such open systems. A main problem is that such CPS apps shall be able to access and modify safety critical device internals. We present results of the TAPPS (Trusted Apps for open CPS) project, which develops an end-to-end solution for development and deployment of trusted apps. The main approach is to devise different execution environments for highly-trusted CPS apps. We present the architecture approach and its key components, and methods for CPS apps, including tool chain and development support.}, doi = {10.1109/EITEC.2016.7503692}, keywords = {cyber-physical systems;open systems;safety-critical software;CPS apps;TAPPS;automotive systems;cyberphysical systems;medical systems;open CPS;open systems;safety critical device internals;tool chain;trusted apps platforms;Automotive engineering;Computer architecture;Electronic mail;Hardware;Real-time systems;Security;Vehicles;architecture;cyber-physical-systems;open-source;real-time systems;trusted apps}, } @inproceedings{, author = {Becker, Klaus and Voss, Sebastian}, title = {A Formal Model and Analysis of Feature Degradation in Fault-Tolerant Systems}, booktitle = {4th Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)}, year = {2016}, month = jan, address = {Paris, France}, abstract = {Fault-tolerant systems have to react on errors resulting from faults properly to avoid error propagation and finally a harmful failure of the entire system. Beside the detection of failing system elements, also the actions to handle failures are essential to cover the safety requirements. Actions reach from enabling fail-silent, fail-safe or fail-operational behavior of system elements, or also hybrids of this in a mixed-critical system design. Graceful degradation may be applied when system resources become insufficient, reducing the set of provided functional features. In this paper we address mixed critical systems, which partially comprise fail-operational functional features. We consider degradations of functional features in failure scenarios. We describe a formal model that contains i.a. the features of a system, possible feature degradations, the software components that realize these features, as well as the deployment of these components to execution units. We calculate valid deployments of software components to execution units and analyze them according to the level of graceful degradation on feature level and system level, as a consequence of failures of execution units or software components. We show an example from the automotive domain to illustrate our approach.}, doi = {10.1007/978-3-319-29510-7_8}, keywords = {Graceful-degradation, Fault-tolerance Redundancy, Fail-operational, Mixed-critical, Diversity, Deployment, Dependability, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Bayha, Andreas and L{\'{u}}cio, Levi and Aravantinos, Vincent and Miyamoto, Kenji and Igna, Georgeta}, title = {Factory Product Lines: Tackling the Compatibility Problem}, booktitle = {Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems (VAMOS)}, publisher = {ACM}, year = {2016}, month = jan, location = {Salvador, Brazil}, abstract = {Variability poses enormous challenges to the manufacturing domain: the demand for highly customized and personalized goods requires bringing a large amount of flexibility to traditional mass production techniques. In particular, when a factory is asked to produce of a new variant of a good, production planning engineers need to manually examine that factory in question, in order to understand whether that new variant can indeed be produced. We call this the "compatibility between the variant and the factory" problem. In this paper, we present a product line-based modelling technique and a tool for assisting production planning engineers in the resolution of this problem.}, doi = {10.1145/2866614.2866623}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Zverlov, Sergey and Khalil, Maged and Chaudhary, Mayank}, title = {Pareto-efficient deployment synthesis for safety-critical applications in seamless model-based development}, booktitle = {Proceedings of the 8th European Congress on Embedded Real Time Software and Systems ({ERTS} 2016)}, series = {Springer in the LNCS series}, year = {2016}, month = jan, abstract = {Increasingly complex functionality in automotive applications demand more and more computing power. As room for computing units in modern vehicles dwindles, centralized ar-chitectures-with larger, more powerful processing units-are the trend. With this trend, applications no longer run on dedicated hardware, but share the same computing resources with others on the centralized platform. Ascertaining efficient deployment and scheduling for co-located applications is complicated by the extra constrains which arise if some of them have a safety-critical functionality. Building on our pre-existing design space exploration solution, we integrated safety constraints, such as ASIL and HW failure rates, as well as practical aspects, such as component costs, and extended the approach to allow for multi-criteria optimization. The work was implemented into our seamless model-based research CASE tool AutoFOCUS3 and evaluated using a non-trivial industrial-inspired case study. The solution is capable of synthesizing deployments together with corresponding schedules, which satisfy different safety and resource constraints. The deployments can subsequently be integrated into the safety case argumentation of AutoFOCUS3, leveraging the tool's seamless capabilities to support safety evidence and certification. Moreover, we are not interested in merely valid solutions, but in good ones. We hence developed a multi-objective optimization algorithm, which synthesizes solutions pareto-optimized for safety, resource usage, timing and any other constraints the user defines. Our approach demonstrates the feasibility and effectiveness of using formal methods to generate correct solutions for safety-critical applications, increasing the confidence and validity of safety cases.}, keywords = {Design Space Exploration, AutoFOCUS, Optimization, SMT, Safety, Resource Optimization, Deployment, Scheduling, Model-based Systems Engineering, MbSE}, url = {https://hal.archives-ouvertes.fr/hal-01289728}, } @inproceedings{Diewald2016, author = {Diewald, Alexander and Voss, Sebastian and Barner, Simon}, title = {A Lightweight Design Space Exploration and Optimization Language}, booktitle = {Proceedings of the 19th International Workshop on Software and Compilers for Embedded Systems (SCOPES '16)}, publisher = {ACM}, pages = {190--193}, year = {2016}, address = {New York, NY, USA}, location = {Sankt Goar, Germany}, abstract = {The solution of many engineering and scientific problems requires the exploration of a huge n-dimensional design space. Typical approaches rely on an abstract problem model consisting of a system model (description of the problem's variable couplings) and an optimization specification defining the objectives as well as the constraints bounding the design space. Advances in solver technologies enabled to efficiently search the solution space, however the diversity of the approaches led to problem descriptions that are difficult to reuse, as well as to solutions that are hard to compare. Our Exploration Meta-Model (EMM) addresses this issue by providing a unified language for optimization specifications that is a well-defined basis for model-based implementations of solver-independent design-space exploration (DSE) tool-chains. The EMM is a light-weight framework that allows to a) describe optimization specifications independent of particular optimization methods and solvers, b) relate solutions and optimization specifications, and c) define domain profiles that provide high-level optimization specifications that ease the adoption of automated DSE by domain experts. The applicability of our framework to different optimization methods is demonstrated by applying it to the generic vector optimization problem and to single-objective linear programs. The EMM's support to relate optimization results to input specifications is exercised for the Opt4J framework. Finally, a profile for real-time embedded systems demonstrates how the EMM can be tailored to specific domains.}, isbn = {978-1-4503-4320-6}, doi = {10.1145/2906363.2906367}, keywords = {AutoFOCUS3, design-space exploration, DSE, model-based systems engineering, MbSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Beyene, Tewodros and Rue{\ss}, Harald}, title = {Integrated Formal Methods for Constructing Assurance Cases}, booktitle = {Proceedings of the 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)}, publisher = {IEEE}, pages = {221--228}, year = {2016}, abstract = {The use of formal methods in verification activities is well established in various dedicated safety standards. Deficits in the verification process may have a negative impact on the confidence of verification results. Safety standards promote the use of integrated formal methods when a single method cannot achieve the verification objective without specifying how. In this paper, we take on the problem of using outputs from integrated formal methods as evidence in assurance cases, which are used in certification of safety-critical systems. We first present two workflows that employ integrated formal methods - code review workflow and code coverage workflow - corresponding to two of the most important activities of the verification phase. Then, we show how each workflow and the outputs from its integrated formal methods can be used in creating an assurance argument. These assurance arguments offer evidence for undeveloped goals identified in previous works from the field.}, doi = {10.1109/ISSREW.2016.21}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {C{\^{a}}rlan, Carmen and Ratiu, Daniel and Sch{\"{a}}tz, Bernhard}, title = {On Using Results of Code-level Bounded Model Checking in Assurance}, booktitle = {Proceedings of the International Conference on Computer Safety, Reliability, and Security (SAFECOMP)}, publisher = {Springer}, series = {LNCS}, volume = {9923}, pages = {30-42}, year = {2016}, abstract = {Software bounded model checkers (BMC) are today powerful tools to perform verification at unit level, but are not used at their potential in the safety critical context. One reason for this is that model checkers often provide only incomplete results when used on real code due to restrictions placed on the environment of the system in order to facilitate the verification. In order to use these results as evidence in an assurance case, one needs to characterize the incompleteness and mitigate the assurance deficits. In this paper we present an assurance case pattern which addresses the disciplined use of successful but possibly incomplete verification results obtained through C-level bounded model checking as evidence in certification. We propose a strategy to express the confidence in incomplete verification results by complementing them with classical testing, and to mitigate the assurance deficits with additional tests. We present our preliminary experience with using the CBMC model checker and the mbeddr environment to verify three safety-critical software components.}, doi = {10.1007/978-3-319-45480-1_3}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Becker, Klaus and Frtunikj, Jelena and Felser, Meik and Fiege, Ludger and Buckl, Christian and Rothbauer, Stefan and Zhang, Licong and Klein, Cornel}, title = {{RACE} {RTE}: A Runtime Environment for Robust Fault-Tolerant Vehicle Functions}, booktitle = {3rd Workshop on Critical Automotive applications - Robustness & Safety (CARS)}, year = {2015}, month = sep, address = {Paris, France}, abstract = {The degree of automated operation in vehicles is increasing continuously. Manufacturers want existing and new functions to be integrated, which drives engineering costs. On the other hand, customers grow accustomed to a steady flow of new functionality on smart phones, partially integrated into their vehicles. In this paper, the Runtime Environment (RTE) of the RACE project is presented. Based on a cross-domain system topology, the RTE executes real-time applications of mixed criticality up to fail-operational behavior. It offers communication and safety mechanisms that are configurable in-field to support Plug&Play scenarios. Since integrated functions often require access to different vehicle domains, the vehicle runtime and configuration data model is reified in the RTE to enable test and verification of all these mechanisms.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://hal.archives-ouvertes.fr/hal-01192987}, } @inproceedings{, author = {Keddis, Nadine and Javed, Bilal and Igna, Georgeta and Zoitl, Alois}, title = {Optimizing Schedules for Adaptable Manufacturing Systems}, booktitle = {IEEE Conference on Emerging Technologies and Factory Automation}, publisher = {IEEE}, year = {2015}, month = sep, abstract = {Adaptability and changeability are becoming the key features of future manufacturing. With adaptability comes a need to dynamically and frequently change factory topologies throughout the life-cycle of manufacturing systems. These changes are necessary to respond to changes in markets that result in new products, production volumes, and product variants. In addition to flexibly switching between different setups, the resulting schedules still have to be optimal to a certain extent to stay profitable. In this paper, we extend a capability-based planning approach to generate timed automata models that are used to solve the scheduling problem. The capability-based approach automatically generates an action sequence that defines all necessary production resources and operations for a product. The action sequence is then automatically transformed into models in UPPAAL - a model-checker for timed automata - and used to generate a schedule for production orders. The result can then be executed on the different production resources. An example scenario based on an industrial production system used for educational purposes shows the suitability of this approach.}, doi = {10.1109/ETFA.2015.7301452}, keywords = {Automata,Job shop scheduling, Production facilities, Optimal scheduling, Schedules, Manufacturing systems, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Kondeva, Antoaneta and Aravantinos, Vincent and Hermanns, Lukas and H{\"{o}}rauf, Leenhard}, title = {The {SFIT} tool: Supporting assembly planners to deal with new product variants}, booktitle = {Proceedings of the 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA)}, publisher = {IEEE}, year = {2015}, month = sep, abstract = {Increasing the number of product variants expected by the customers; decreasing product life cycles; operating existing production systems as long as possible, all these factors make the planning of new or the reconfiguration of existing assembly systems a complex and time-consuming task. Yet assembly planners lack adequate tool support in taking the right decisions by such competitive goals and to handle this complexity. In this paper, we present a tool which supports the modelling of the different relevant aspects in a clearly independent way such as products, assembly lines, processes and especially the explicit relationships between these aspects such as which process step is executed on which station or which part is used in which process step. Having the information clearly input by the user, various analyses can be provided to support the assembly planner in his/her design decisions.}, doi = {10.1109/ETFA.2015.7301646}, keywords = {product, assembly planning support, automatic consistency checking, part variants, model-based systems engineering, MbSE}, } @article{Teufl2015, author = {Teufl, Sabine and Hackenberg, Georg}, title = {Efficient Impact Analysis of Changes in the Requirements of Manufacturing Automation Systems}, publisher = {Elsevier}, journal = {IFAC Proceedings Volumes}, volume = {48}, number = {3}, pages = {1482--1489}, year = {2015}, month = aug, timestamp = 2015.08.31, owner = {teufl}, address = {Ottawa, Canada}, abstract = {Various drivers, especially increasing market dynamics, force industrial enterprises to evolve their production facilities ever more frequently. Analyzing the impact of changed requirements on the production facilities early in the engineering process would facilitate the estimation of resulting costs and therefore reduce project risk. In industrial practice, requirements specifications are typically textual lists and only structured by a table of contents; an analysis of the impact of changes within the requirements specification is extensive, as no documented information is available about how the requirements and other elements of the requirements specification depend on each other. To identify impacts of changes in a requirements specification more efficiently, this paper proposes a model-based approach that classifies the elements of a requirements specification according to their contents and based on the classification preselects automatically candidate elements of the requirements specification that are possibly affected by the change. This paper shows the application of the approach on the manufacturing automation systems domain by means of a pick and place unit (PPU) demonstrator. The technical validation demonstrates that in the example of the PPU the impact analysis is more efficient with a content model than on an unstructured list; the effort for impact analysis is reduced further when adapting the content model to the manufacturing automation systems domain.}, doi = {10.1016/j.ifacol.2015.06.296}, keywords = {Model-based Requirements Engineering, Requirements Analysis, Impact Analysis, Manufacturing System, Knowledge Acquisition, Systems Engineering}, } @inproceedings{, author = {Gupta, Pragya Kirti and Becker, Klaus and Duchon, Markus and Sch{\"{a}}tz, Bernhard}, title = {Formalizing Performance Degradation Strategies as an Enabler for Selfhealing Smart Energy Systems}, booktitle = {{Tagungsband Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme XI Model-Based Development of Embedded Systems}}, year = {2015}, month = apr, organization = {Dagstuhl-Workshop MBEES: Eleventh Workshop on Modellbasierte Entwicklung Eingebetteter Systeme}, abstract = {Smart behavior in reactive systems can be achieved when systems can react appropriately to environmental changes. These adjustments in behavior can be achieved through predefined strategies. In this work, we present a formal specification of performance degradation where the overall performance of the system is intentionally lowered in order to ensure high availability of the core services of the system in fault scenarios. We demonstrate the application of this strategy in the energy domain. Power outages can be foreseen as one of the big challenges in the smart grid functionality. In such a power outage situation, it is essential to support high priority services at all times. During such situations, to prolong support for high priority services , we propose an approach using constraint-based formal modeling by developing the degradation strategy. A service is selected or deactivated based on its priority, energy consumption and its performance contribution. As a consequence, when services have to be disabled due to insufficient available energy, the performance of the overall system degrades, but high priority services remain available. We validate our approach by using the Z3 SMT solver to identify a valid degradation strategy scheme for a fault scenario in the fortiss smart energy living lab demonstrator.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://download.fortiss.org/public/mbees/mbees2015_proceedings.pdf}, } @inproceedings{, author = {Voss, Sebastian and C{\^{a}}rlan, Carmen and Sch{\"{a}}tz, Bernhard and Kelly, Tim}, title = {Safety Case Driven Model-Based Systems Construction}, booktitle = {Proceedings of the 2nd International IFIP Workshop on Emerging Ideas and Trends in Engineering of Cyber-Physical Systems (EITEC 2015)}, year = {2015}, month = apr, location = {Seattle, USA}, keywords = {Model-based Systems Engineering, MbSE}, url = {http://eitec.informatik.tu-muenchen.de/2015/program.html}, } @inproceedings{becker2015a, author = {Becker, Klaus and Sch{\"{a}}tz, Bernhard}, title = {Deployment Calculation and Analysis for a Fault-Tolerant System Platform}, booktitle = {11th Dagstuhl-Workshop on Model-Based Development of Embedded Systems (MBEES)}, pages = {100-109}, year = {2015}, month = mar, abstract = {In many embedded systems like in the automotive domain, safety-critical features are increasingly realized by software. Some of these features are often required to behave fail-operational, meaning that they must stay alive even in the presence of random hardware failures. In this paper, we introduce a constraint-based approach to calculate valid deployments of mixed critical software components to the execution nodes of a new fault-tolerant SW/HW architecture for electric vehicles. To avoid harm, faulty execution nodes have to be isolated from the remaining system. We treat the changes to the deployment that are required after isolations of execution nodes to keep those software components alive that realize fail-operational features. However, the remaining system resources may become insufficient to execute the full set of software components after such isolations. Hence, some components might have to be deactivated, meaning that features might get lost. Our approach allows to formally analyze which subset of features can still be provided after one or more isolations. We present an arithmetic system model of the deployment problem that can be solved by an SMT solver.}, keywords = {Fault-tolerance, fail-operational, deployment, model-based systems engineering, MbSE}, url = {https://mediatum.ub.tum.de/doc/1281559/288733.pdf}, } @inproceedings{, author = {V{\"{o}}gele, Christian and van Hoorn, Andr{\'{e}} and Krcmar, Helmut}, title = {Automatic Extraction of Session-Based Workload Specifications for Architecture-Level Performance Models.}, booktitle = {Proceedings of the International Workshop on Large-Scale Testing}, publisher = {ACM}, pages = {5-8}, year = {2015}, month = feb, location = {Austin, Texas, USA}, keywords = {Load Tests, Palladio Component Model, Session- based Application Systems, Workload Specications}, } @inproceedings{Buechel2015, author = {Buechel, Martin and Frtunikj, Jelena and Becker, Klaus and Sommer, Stephan and Buckl, Christian and Armbruster, Michael and Klein, Cornel and Marek, Andre and Zirkler, Andreas and Knoll, Alois}, title = {An Automated Electric Vehicle Prototype Showing New Trends in Automotive Architectures}, booktitle = {IEEE 18th International Conference on Intelligent Transportation Systems (ITSC)}, year = {2015}, location = {Las Palmas, Gran Canaria, Spain}, abstract = {The automotive domain is challenged by the increasing importance of Information Technology (IT) based functions. To show the possibilities of modern IT systems, a demonstrator car was developed in RACE (Robust and Reliant Automotive Computing Environment for Future eCars) based on a completely redesigned E/E architecture, which supports the integration of mixed-criticality components and offers features like Plug&Play. This paper presents the architecture and components of this vehicle prototype, which is equipped with modern systems such as Steer-by-Wire without mechanical fallback. It was designed to support future driver assistance systems, e.g. to carry out autonomous parking maneuvers onto an inductive charging station, a task, which is hard to achieve accurately enough for a human driver. Therefore, a special emphasis lies on the description of the sensor set for automated operation.}, doi = {10.1109/ITSC.2015.209}, keywords = {Automated Vehicles, automotive architecture, autonomous driving, electric vehicle, Vehicle Prototype, Model-based Systems Engineering, MbSE}, } @inproceedings{becker2015b, author = {Becker, Klaus and Voss, Sebastian}, title = {Analyzing Graceful Degradation for Mixed Critical Fault-Tolerant Real-Time Systems}, booktitle = {18th IEEE Symposium on Real-Time Distributed Computing (ISORC)}, publisher = {IEEE}, year = {2015}, location = {Auckland, New Zealand}, abstract = {Fault-tolerant distributed embedded systems have to react properly on the occurrence of faults in order to avoid harm to the system or its environment. Faulty system resources have to be isolated from the remaining system. Hence, these resources become unavailable, leading to a decreasing number of available resources and input data. In such cases, mechanisms like graceful degradation may be applied to ensure that the system does not turn off completely, but degrades its provided set of functional features gracefully. It must be ensured that the remaining intact resources are efficiently used to execute at least those features, which are required to behave fail-operational. In this paper, we investigate deployments of mixed-critical software components to a fault-tolerant system platform. We introduce a formal model of software components and their publish/subscribe based communication channels. We use this model to analyze the graceful degradation of the system in different scenarios of failing execution hardware. This includes also the explicit deactivation of software components due to unavailable required input data. Our analysis is based on using an SMT solver and contributes to guarantee that all requirements with respect to fail-operationality are met by the system design. The approach is evaluated by an example and a scalability analysis.}, doi = {10.1109/ISORC.2015.10}, keywords = {Dependability, Fault Tolerance, Graceful Degradation, Mixed Criticality, Deployment, Formal Methods, SMT, Model-based Systems Engineering, MbSE}, } @incollection{, author = {Aravantinos, Vincent and Voss, Sebastian and Teufl, Sabine and H{\"{o}}lzl, Florian and Sch{\"{a}}tz, Bernhard}, title = {AutoFOCUS 3: Tooling Concepts for Seamless, Model-based Development of Embedded Systems}, booktitle = {ACES-MB&WUCOR@MoDELS 2015}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, pages = {19-26}, year = {2015}, abstract = {This paper presents tooling concepts in AutoFOCUS 3 supporting the development of software-intensive embedded system design. AutoFOCUS 3 is a highly integrated model-based tool covering the complete development process from requirements elicitation, deployment, the modelling of the hardware platform to code generation. This is achieved thanks to precise static and dynamic semantics based on the FOCUS theory. Models are used for requirements, for the software architecture (SA), for the hardware platform and for relations between those different viewpoints: traces from requirements to the SA, refinements between SAs, and deployments of the SA to the platform. This holistic usage of models allows the provision of a wide range of analysis and synthesis techniques such as testing, model checking and deployment and scheduling generation. In this paper, we demonstrate how tooling concepts on different steps in the development process look like, based on these integrated models and implemented in AutoFOCUS 3.}, keywords = {AutoFOCUS3, Seamless MBD, Model-Based Development, Embedded Systems, Tooling Concept, Tooling, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-1508/paper4.pdf}, } @inproceedings{schaetz2015, author = {Sch{\"{a}}tz, Bernhard and Zverlov, Sergey and Voss, Sebastian}, title = {Automating Design-Space Exploration: Optimal Deployment of Automotive SW-Components in an ISO26262 Context}, booktitle = {Design Automation Conference (DAC), 2015 52st ACM/EDAC/IEEE}, year = {2015}, abstract = {With a growing demand for complex, safety-critical features in automotive vehicles, functional safety is a key issues of automotive software development. Consequently, standards like ISO26262 propose methods and techniques for the systematic development of automotive software. Furthermore, the growing amount of functionality - including active safety systems or automated driver assistance functions - on the control of the vehicle dynamics and the correspondingly used more powerful electronic platforms requires methods supporting the development of systems in an increasingly complex design space. In this contribution, an approach is presented that supports the allocation of software functions to hardware elements in an automated fashion, respecting the separation constraints concerning assurances levels.}, doi = {10.1145/2744769.2747912}, keywords = {AutoFOCUS3, design-space exploration, DSE, deployment synthesis, mapping, model-based systems engineering, MbSE}, } @inproceedings{, author = {Aravantinos, Vincent and Miyamoto, Kenji and Molotnikov, Zaur and Regnat, Nikolaus and Sch{\"{a}}tz, Bernhard}, title = {Textual model-based software/system architecture documentation using MPS}, booktitle = {Software Engineering & Management}, volume = {239}, pages = {232-237}, year = {2015}, location = {Dresden, Germany}, abstract = {A system architecture provides essential communication means between the architect and the user of the system diminishing thus the risk of misunderstanding during the development phase. In many domains, the tools used for documentation are word processors, typically Microsoft Word. However such tools allow to manipulate text with little structure only thus potentially yielding many inconsistencies in the document. In this paper, we report on a case study making use of textual models and model-based editors in order to develop such a documentation system for Siemens AG. We propose here to transfer these techniques to a new domain: (non-necessarily software) system documentation. The use of models allows to introduce more semantics into the editor, with the concrete effect of imposing more structure on the document to ensure the consistency of the document and thus prevent issues earlier in the development. We implemented the above process using the model-based programming environment MPS.}, isbn = {978-3-88579-633-6}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://dl.gi.de/handle/20.500.12116/2556}, } @inproceedings{, author = {van Hoorn, Andr{\'{e}} and V{\"{o}}gele, Christian and Schulz, Eike and Hasselbring, Wilhelm and Krcmar, Helmut}, title = {Automatic Extraction of Probabilistic Workload Specifications for Load Testing Session-Based Application Systems}, booktitle = {Proceedings of the 8th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2014)}, publisher = {ACM}, year = {2014}, month = nov, location = {Bratislava, Slovakia}, keywords = {Clustering, Load Test Extraction, load testing, Session- based Application Systems, Workload Specications}, } @inproceedings{bytschkow2014, author = {Bytschkow, Denis and Quilbeuf, Jean and Igna, Georgeta and Rue{\ss}, Harald}, title = {Distributed MILS architectural approach for secure smart grids}, booktitle = {Smart Grid Security}, publisher = {Springer International Publishing}, pages = {16--29}, year = {2014}, month = aug, abstract = {Successful decentralized and prosumer-based smart grids need to be at least as dependable and secure as the prevailing one-way, generation-transmission-distribution-consumer power grids. With this motivation in mind, we propose a two-phase model-based design methodology for secure architectural design and secure deployment of such a security architecture on a distributed separation kernel. In particular, we are modeling essential parts of a smart micro grid with several interacting prosumers, and demonstrate exemplary security/privacy requirements of this smart grid. The security policy architecture of this smart grid is deployed on a secure distributed platform, relying on a combination of separation kernels and deterministic network, as developed in the Distributed MILS project.}, doi = {10.1007/978-3-319-10329-7_2}, keywords = {Smart grid security, Distributed MILS, Separation kernel, Formal verification, Security policy architecture, Configuration compiler, Model-based Systems Engineering, MbSE}, } @inproceedings{Teufl2014, author = {Teufl, Sabine and B{\"{o}}hm, Wolfgang and Pinger, Ralf}, title = {Understanding and closing the gap between requirements on system and subsystem level}, booktitle = {Model-Driven Requirements Engineering Workshop (MoDRE), 2014 IEEE 4th International}, pages = {77-86}, year = {2014}, month = aug, timestamp = 2014.09.23, owner = {teufl}, abstract = {In systems engineering, the increasing complexity of systems is handled by decomposing systems into subsystems. As part of the decomposition typically more abstract system requirements are refined to more detailed subsystem requirements. Refining system requirements to subsystem requirements includes the two steps interface refinement on the system boundaries, and a decomposition of system requirements to subsystem requirements. In order to apply formal analysis and verification techniques on the refinement of requirements, a formal refinement specification is necessary. In this paper we show the results of an exploratory industrial case study provided by Siemens, where we analyzed the refinement from system to subsystem requirements. We show that formal refinement specifications can become very complex, when interface refinement and requirement decompositions are performed in one step. In order to reduce complexity in the formal refinement specification, we introduce a formal restructuring approach for requirements. The main benefits of this restructuring approach are twofold. It enables reuse of requirements and knowledge preservation on the system level when the system architecture changes. Furthermore, quality assurance of the refinement on system level can now be performed independently from the system decomposition.}, doi = {10.1109/modre.2014.6890828}, keywords = {abstract system requirements, Abstracts, Analytical models, Case study, Complexity theory, formal analysis, formal refinement specification, formal restructuring approach, formal specification, formal verification, formal verification techniques, knowledge preservation, Modelling language, Quality assurance, Requirements engineering, requirements reuse, Siemens, subsystem requirements, Syntactics, system architecture, system decomposition, systems engineering}, } @inproceedings{KrWo:Cloud:2014, author = {Kro{\ss}, Johannes and Wolke, Andreas}, title = {Cloudburst - Simulating Workload for IaaS Clouds}, booktitle = {Proceedings of the 2014 IEEE 7th International Conference on Cloud Computing}, publisher = {IEEE}, series = {CLOUD '14}, pages = {841--848}, year = {2014}, month = jun, location = {Anchorage, Alaska, USA}, abstract = {In this work we implemented Cloudburst to generate realistic workload in Infrastructure as a Service cloud testbeds. Our goal was to minimize the memory footprint of such workload generators by leveraging alternative programming paradigms for highly concurrent applications. In contrast to many existing we leverage the concurrency model of the Go programming language instead of threads. Initial benchmarks with Cloudburst and Rain suggest that Cloudburst consumes significantly less memory at the cost of a higher CPU footprint. In our experimental testbed memory is a more critical resource. Leveraging Cloudburst allows us to run larger benchmarks with the same hardware.}, isbn = {978-1-4799-5062-1}, doi = {10.1109/CLOUD.2014.116}, keywords = {benchmark, Benchmark testing, cloud computing, Cloudburst, Clouds, concurrency control, Generators, Go programming language concurrency model, IaaS clouds, infrastructure as a service cloud testbeds, Java, load driver, memory footprint minimization, Message systems, Rain, Servers, virtual machines}, url = {http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6973822}, } @inproceedings{becker2014, author = {Becker, Klaus and Armbruster, Michael and Sch{\"{a}}tz, Bernhard and Buckl, Christian}, title = {Deployment Calculation and Analysis for a Fail-Operational Automotive Platform}, booktitle = {1st Workshop on Engineering Dependable Systems of Systems (EDSoS)}, year = {2014}, month = may, location = {Newcastle upon Tyne, UK}, abstract = {In domains like automotive, safety-critical features are increasingly realized by software. Some features might even require fail-operational behavior, so that they must be provided even in the presence of random hardware failures. A new fault-tolerant SW/HW architecture for electric vehicles provides inherent safety capabilities that enable fail-operational features. In this paper we introduce a formal model of this architecture and an approach to calculate valid deployments of mixed-critical software-components to the execution nodes, while ensuring fail-operational behavior of certain components. Calculated redeployments cover the cases in which faulty execution nodes have to be isolated. This allows to formally analyze which set of features can be provided under decreasing available execution resources.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://arxiv.org/abs/1404.7763}, } @inproceedings{, author = {Pfaff, Matthias and Krcmar, Helmut}, title = {Semantic Integration of Semi-Structured Distributed Data in the Domain of IT Benchmarking - Towards a Domain Specific Ontology}, booktitle = {16th International Conference on Enterprise Information Systems (ICEIS 2014)}, publisher = {SciTePress}, pages = {320-324}, year = {2014}, month = apr, location = {Lisboa}, abstract = {In the domain of IT benchmarking a variety of data and information are collected. The collection of this heterogeneous data is usually done in the course of specific benchmarks (e.g. focusing on IT service management topics). This collected knowledge needs to be formalized previous to any data integration, in order to ensure interoperability of different and/or distributed data sources. Even though these data are the basis to identify potentials for IT cost reductions or IT service improvements, a semantic data integration is missing. Building on previous research in IT benchmarking we emphasise the importance of further research in data integration methods. Before we describe why the next step of research needs to focus on the semantic integration of data that typically resides in IT benchmarking, the evolution of IT benchmarking is outlined first. In particular, we motivate why an ontology is required for the domain of IT benchmarking.}, doi = {10.5220/0004969303200324}, keywords = {Coupling and Integrating Heterogeneous Data Sources, Data Mining, Distributed Database Systems}, } @article{Huang2014, author = {Huang, Jia and Barner, Simon and Raabe, Andreas and Buckl, Christian and Knoll, Alois}, title = {A framework for reliability-aware embedded system design on multiprocessor platforms}, journal = {Microprocessors and Microsystems}, volume = {38}, number = {6}, pages = {539--551}, year = {2014}, month = mar, abstract = {This paper presents a model-driven framework that provides a tool-supported design flow for fault-tolerant embedded systems. Its system models comprise abstract descriptions of the application and the underlying execution platform. They provide the input to our analysis and optimization techniques that enable the automated exploration of design alternatives for applications with reliability requirements. The automated generation of source code and platform configuration files speeds up the development process. Our contribution is to advance reliability-aware design further into practice by providing an integrated tool framework and removing unrealistic assumptions in the analyzes. The case studies demonstrate the effectiveness of our approach.}, issn = {0141-9331}, doi = {10.1016/j.micpro.2014.02.007}, keywords = {Embedded systems; Reliability; Fault-tolerance ; Design optimization; Model-driven development}, } @inproceedings{voss2014design, author = {Voss, Sebastian and Eder, Johannes and H{\"{o}}lzl, Florian}, title = {Design Space Exploration and its Visualization in AutoFOCUS3}, booktitle = {Software Engineering (Workshops)}, pages = {57--66}, year = {2014}, month = feb, abstract = {Software-intensive embedded systems are characterized by an increasing number of features that implement complex safety-critical functionalities. These systems are more and more developed in a model-based fashion that has been considered as a central design approach to deal with the increase in software complexity. These kinds of embedded systems always require multiple constraints both functional and non-functional ones. AutoFOCUS3 is a model-based development framework using tightly integrated models that enable to perform design space exploration for multi-criteria problems. Finding suitable deployments, meaning the (efficient) assignment of software components to hardware components, is one of these problems. This paper illustrates how such a Design Space Exploration approach in a model-based framework can support the system designer in a (semi-) automatic way, enabling to compare different valid design solutions, w.r.t. a set of given system requirements. We propose a visualization technique to efficiently guide the system designer through such a calculated solutions space. The presented approach has been implemented in the AutoFOCUS3 framework.}, keywords = {AutoFOCUS3, design-space exploration, DSE, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-1129/paper33.pdf}, } @inproceedings{becker2014b, author = {Becker, Klaus and Sch{\"{a}}tz, Bernhard and Armbruster, Michael and Buckl, Christian}, title = {A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant Systems}, booktitle = {Proceedings of the 12th International Conference on Software Engineering and Formal Methods (SEFM)}, year = {2014}, location = {Grenoble, France}, abstract = {In many embedded systems like in the automotive domain, safety-critical features are increasingly realized by software. Some of these features are often required to behave fail-operational, meaning that they must stay alive even in the presence of random hardware failures. We propose a new fault-tolerant SW/HW architecture for electric vehicles with inherent safety capabilities that enable fail-operational features. In this paper, we introduce a constraint-based approach to calculate valid deployments of mixed-critical software components to the execution nodes. To avoid harm, faulty execution nodes have to be isolated from the remaining system. We treat the isolations of execution nodes and the required changes to the deployment to keep those software components alive that realize fail-operational features. The affected software components have to be resumed on intact execution nodes. However, the remaining system resources may become insufficient to execute the full set of software components after an isolation of an execution node. Hence, some components might have to be deactivated, meaning that features might get lost. Our approach allows to formally analyze which subset of features can still be provided after one or more isolations. We present an arithmetic system model with formal constraints of the deployment-problem that can be solved by a SMT-Solver. We evaluate our approach by showing an example problem and its solution.}, doi = {10.1007/978-3-319-10431-7_15}, keywords = {Fault-Tolerance, Fail-Operational, Mixed-Critical, Deployment, Dependability, SMT, Model-based Systems Engineering, MbSE}, } @inproceedings{MK_ERTS_2014, author = {Khalil, Maged and Sch{\"{a}}tz, Bernhard and Voss, Sebastian}, title = {A Pattern-based Approach towards Modular Safety Analysis and Argumentation}, booktitle = {Embedded Real Time Software and Systems Conference (ERTS 2014), Toulouse, France}, year = {2014}, abstract = {Safety standards recommend (if not dictate) performing many analyses during the concept phase of development as well as the early adoption of multiple measures at the architectural design level. In practice, the reuse of architectural measures or safety mechanisms is widely-spread, especially in well-understood domains, as is reusing the corresponding safety-cases aiming to document and prove the fulfillment of the underlying safety goals. Safety-cases in the automotive domain are not well-integrated into architectural models and as such do not provide comprehensible and reproducible argumentation nor any evidence for argument correctness. The reuse is mostly ad-hoc, with loss of knowledge and traceability and lack of consistency or process maturity as well as being the most widely spread and cited drawbacks. Using a simplified description of software functions and their most common error management subtypes (avoidance, detection, handling, ..) we propose to define a pattern library covering known solution algorithms and architectural measures/constraints in a seamless holistic model-based approach with corresponding tool support. The pattern libraries would comprise the requirement the pattern covers and the architecture elements/ measures / constraints required and may include deployment or scheduling strategies as well as the supporting safety case template, which would then be integrated into existing development environments. This paper explores this approach using an illustrative example.}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{MK_IMBSA_2014, author = {Khalil, Maged and Prieto, Alejandro and H{\"{o}}lzl, Florian}, title = {A pattern-based approach towards the guided reuse of safety mechanisms in the automotive domain}, booktitle = {Proceedings of the International Symposium on Model-Based Safety and Assessment ({IMBSA} 2014)}, publisher = {Springer}, series = {LNCS}, volume = {8822}, pages = {137--151}, year = {2014}, abstract = {The reuse of architectural measures or safety mechanisms is widely-spread in practice, especially in well-understood domains, as is reusing the corresponding safety-case to document the fulfillment of the target safety goal(s). This seems to harmonize well with the fact that safety standards recommend (if not dictate) performing many analyses during the concept phase of development as well as the early adoption of multiple measures at the architectural design level. Yet this front-loading is hindered by the fact that safety argumentation is not well-integrated into architectural models in the automotive domain and as such does not support comprehensible and reproducible argumentation nor any evidence for argument correctness. The reuse is neither systematic nor adequate. Using a simplified description of safety mechanisms, we defined a pattern library capturing known solution algorithms and architectural measures/constraints in a seamless holistic model-based approach with corresponding tool support. Based on a meta-model encompassing both development artifacts and safety case elements, the pattern library encapsulates all the information necessary for reuse, which can then be integrated into existing development environments. This paper explores the model and the approach using an illustrative implementation example, along with the supporting workflow for the usage of the approach in both “designer” and “user” roles.}, doi = {10.1007/978-3-319-12214-4_11}, keywords = {Safety-critical systems, pattern-based design, architectures, safety cases, automotive, reuse, Model-based Systems Engineering, MbSE}, } @inproceedings{voss2014dse, author = {Voss, Sebastian and Zverlov, Sergey}, editor = {Mař{\'{i}}k, Vladim{\'{i}}r and Lastra, JoseL. Martinez and Skobelev, Petr}, title = {Design Space Exploration in AutoFOCUS3 - An Overview}, booktitle = {IFIP First International Workshop on Design Space Exploration of Cyber-Physical Systems}, year = {2014}, organization = {Springer}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{Diebold:2014:PRE:2601248.2601250, author = {Diebold, Philipp and Lampasona, Constanza and Zverlov, Sergey and Voss, Sebastian}, title = {Practitioners' and Researchers' Expectations on Design Space Exploration for Multicore Systems in the Automotive and Avionics Domains: A Survey}, booktitle = {Proceedings of the 18th International Conference on Evaluation and Assessment in Software Engineering}, publisher = {ACM}, series = {EASE '14}, pages = {1:1--1:10}, year = {2014}, address = {New York, NY, USA}, location = {London, England, United Kingdom}, abstract = {Background: The mobility domains are moving towards the adoption of multicore technology. Appropriate methods, techniques, and tools need to be developed or adapted in order to fulfill the existing requirements. This is a case for design space exploration methods and tools. Objective: Our goal was to understand the importance of different design space exploration goals with respect to their relevance, frequency of use, and tool support required in the development of multicore systems from the point of view of the ARAMiS project members. Our aim was to use the results to guide further work in the project. Method: We conducted a survey regarding the current state of the art in design space exploration in industry and research and collected the expectations of project members regarding design space exploration goals. Results: The results show that design space exploration is an important topic in industry as well as in research. It is used very often with different important goals to optimize the system. Conclusions: Current tools provide only partial solutions for design space exploration. Our results can be used for improving them and guiding their development according to the priorities explained in this contribution.}, isbn = {978-1-4503-2476-2}, doi = {10.1145/2601248.2601250}, keywords = {automotive, avionics, design space exploration, industry, multicore, research, Survey, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Zverlov, Sergey and Voss, Sebastian}, title = {Synthesis of Pareto Efficient Technical Architectures for Multi-core Systems}, booktitle = {Computer Software and Applications Conference Workshops (COMPSACW), 2014 IEEE 38th International}, year = {2014}, abstract = {In the area of embedded systems exists a continuous need for more computing power while still fulfilling a large set of constraints in - for instance - timing, safety, cost and energy consumption. Since single-core technologies seem to reach their limits, multi-core systems became the trend in this area. This paper describes a synthesis approach of application-specific homogeneous multi-core architectures, which are optimized towards timing, number of cores and energy consumption. Our method finds the optimal number of cores of the multi-processor system, along with the mapping of tasks onto these cores with the corresponding schedules and the frequency for each core. Since the optimization criteria are concurrent, the results are presented as a Pareto front. The approach is integrated in the model-based tooling framework, called Auto FOCUS3. As input our approach uses the information from the logical architecture of AF3, which represents a component based structure view of the system under development. The approach is based on the Branch & Bound algorithm, which was adapted for our three-dimensional optimization problem.}, doi = {10.1109/COMPSACW.2014.63}, keywords = {AutoFOCUS3, design-space exploration, DSE, architecture synthesis, HW/SW co-design, model-based systems engineering, MbSE}, } @inproceedings{Sommer2013b, author = {Sommer, Stephan and Camek, Alexander and Buckl, Christian and Becker, Klaus and Zirkler, Andreas and Fiege, Ludger and Armbruster, Michael and Knoll, Alois}, title = {RACE: A Centralized Platform Computer Based Architecture for Automotive Applications}, booktitle = {Vehicular Electronics Conference (VEC) and the International Electric Vehicle Conference (IEVC) (VEC/IEVC 2013)}, publisher = {{IEEE}}, year = {2013}, month = oct, abstract = {In the last couple of years software functionality of modern cars increased dramatically. This growing functionality leads directly to a higher complexity of development and configuration. Current studies show that the amount of software will continue to grow. Additionally, advanced driver assistance systems (ADAS) and autonomous functionality, such as highly and fully automated driving or parking, will be introduced. Many of these new functions require access to different communication domains within the car, which increases system complexity. AUTOSAR, the software architecture established as a standard in the automotive domain, provides no methodologies to reduce this kind of complexity and to master new challenges. One solution for these evolving systems is developed in the RACE project. Here, a centralized platform computer (CPC) is introduced, which is inspired by the well-established approach used in other domains like avionics and automation. The CPC establishes a generic safety-critical execution environment for applications, providing interfaces for test and verification as well as a reliable communication infrastructure to smart sensors and actuators. A centralized platform also significantly reduces the complexity of integration and verification of new applications, and enables the support for Plug&Play.}, doi = {10.1109/IEVC.2013.6681152}, keywords = {embedded, RACE, Model-based Systems Engineering, MbSE}, } @techreport{quilbeuf2013, author = {Quilbeuf, Jean and Igna, Georgeta and Bytschkow, Denis and Rue{\ss}, Harald}, title = {Security policies for distributed systems}, journal = {arXiv preprint}, volume = {arXiv:1310.3723}, year = {2013}, month = oct, school = {arXiv preprint}, abstract = {A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run in separation, and possible process communication on a technical platform is restricted to specified message paths of the system. Furthermore, we propose to further restrict the allowable information flow by adding filter functions for controlling which messages may be transmitted between processes, and we prove that locally checking filter functions is sufficient for ensuring global security policies. Altogether, global intransitive security policies are established by means of local verification conditions for the (trusted) processes of the distributed system. Moreover, security policies may be implemented securely on distributed integration platforms which ensure partitioning. We illustrate our results with a smart grid case study, where we use CTL model checking for discharging local verification conditions for each process under consideration.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://arxiv.org/abs/1310.3723}, } @article{Barner2013, author = {Barner, Simon and Huang, Jia and Voss, Sebastian}, title = {Sicher steuern mit Multicore-Prozessoren}, journal = {Computer & Automation}, pages = {24-29}, year = {2013}, month = jun, note = {Control \& Drives 2013.}, abstract = {Multicore-Prozessoren bieten sich in der Automatisierung vor allem zur Integration von Steuerungsprogrammen und somit zur Reduktion der Anzahl von Steuerger{\"{a}}ten an. Insbesondere wenn es um sicherheitskritische Anwendungen geht, ist dabei allerdings zu gew{\"{a}}hrleisten, dass die verschiedenen Anwendungen hinreichend voneinander separiert sind. Die modellbasierte Entwicklung leistet hier wertvolle Unterst{\"{u}}tzung.}, keywords = {Model-based Systems Engineering, MbSE}, url = {http://www.computer-automation.de/steuerungsebene/industrie-pc/artikel/97588/}, } @inproceedings{, author = {Kelly, Tim and C{\^{a}}rlan, Carmen and Voss, Sebastian}, title = {Model-Based Safety Cases in AutoFOCUS3 (Tool Demonstration)}, booktitle = {Proceedings of the 1st International Workshop on Assurance Cases for Software-intensive Systems ({ASSURE} 2013)}, year = {2013}, month = may, keywords = {AutoFOCUS3, model-based safety cases, ExplicitCase, model-based systems engineering, MbSE}, url = {https://www.cs.york.ac.uk/assure2013/Program.html}, } @inproceedings{, author = {Voss, Sebastian and Sch{\"{a}}tz, Bernhard}, title = {Deployment and Scheduling Synthesis for Mixed-Critical Shared Memory Applications}, booktitle = {Proceedings of the Engineering Computer-Based Systems Conference ({ECBS} '13)}, publisher = {IEEE}, pages = {100--109}, year = {2013}, month = apr, address = {Phoenix, AZ, USA}, abstract = {This paper presents an efficient approach for generating suitable system architectures for embedded systems efficiently. Thereby, we focus on a joint generation of schedules and deployment for mixed-criticality multicore architectures using shared memory. The presented approach computes task and message schedules that are optimized with respect to a global discrete time base. As part of the solution, our approach generates an optimized assignment of tasks to computation resources (cores) concerning local memory constraints of cores and criticality constraints of tasks.This approach is integrated into the Auto FOCUS3 tool-chain, using a formally defined model of computation with explicit data-flow and discrete-time semantics to develop multi-criticality embedded systems. Our approach relies on a symbolic encoding scheme, based on a system model that is derived from the system architecture. This paper provides a formalization describing the scheduling problem as a satisfiability problem using boolean formulas and linear arithmetic constraints. A state-of-the-art satisfiability modulo theory (SMT) solver is used to compute the joint schedule and deployment for such architectures. This paper demonstrates that state-of-the art satisfiability modulo theory solvers can be used to efficiently compute (safety-oriented) deployments including real-time task and communication schedules for mixed-criticality applications.}, doi = {10.1109/ECBS.2013.23}, keywords = {deployment synthesis, mapping, scheduling, shared-memory applications, SMT, AutoFOCUS3, design-space exploration, DSE, model-based systems engineering, MbSE}, } @inproceedings{, author = {Voss, Sebastian and Kondeva, Antoaneta and Ratiu, Daniel and Sch{\"{a}}tz, Bernhard}, title = {Seamless Model-based Development of Embedded Systems with {AF3} Phoenix}, booktitle = {Tool demonstration on the 20th Annual {IEEE} International Conference and Workshops on the Engineering of Computer Based Systems ({ECBS})}, pages = {212}, year = {2013}, month = apr, abstract = {To effectively and efficiently use a model-based development process, tools must offer integrated system views on several levels of abstraction, and provide useable sophisticated analysis and synthesis techniques. We demonstrate how these features are implemented for the development of embedded systems in AF3 Phoenix.}, doi = {10.1109/ECBS.2013.20}, keywords = {AutoFOCUS3, methodology, tooling, model-based systems engineering, MbSE}, } @inproceedings{, author = {Hattendorf, Anton and Voss, Sebastian}, title = {Emergency Shutdown System Demonstrator using {AutoFOCUS3}}, booktitle = {Proceedings of the {W8} Workshop on Industry-Driven Approaches for Cost-effective Certification of Safety-Critical, Mixed-Criticality Systems ({WICERT}) (co-located with {DATE})}, year = {2013}, abstract = {For safety critical applications, separation is needed in hardware and software. The model based development tool AutoFocus 3 supports design, simulation and verification of safety critical applications. It uses a hierarchical component based model and provides a complete tool chain from application design to running code. Our separation platform provides spatial and temporal separation in a shared memory architecture. Temporal separation is archived through a special DDR2 arbiter, while spatial separation is enforced through a MPU that guards the shared memory. The Emergency Shutdown System Demonstrator - jointly implemented by Danfoss Drives and fortiss GmbH - implements a software controlled emergency shutdown system. It uses a dual core architecture. All inputs are forwarded to both cores. When the emergency switch is hit, both cores independently shut down the system. The application logic is designed and verified using AF3. The application components are deployed to the cores. Finally the automated code generation of the AF3 tool chain is used to bring the application to the hardware.}, keywords = {AutoFOCUS3, Danfoss, Emergency Shutdown, Demonstrator, Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Pop, Paul and Tsiopoulos, Leonidas and Voss, Sebastian and Slotosch, Oscar and Ficek, Christoph and Nyman, Ulrik and Lopez, Alejandra Ruiz}, title = {Methods and tools for reducing certification costs of mixed-criticality applications on multi-core platforms: the {RECOMP} approach}, booktitle = {Proceedings of the {W8} Workshop on Industry-Driven Approaches for Cost-effective Certification of Safety-Critical, Mixed-Criticality Systems ({WICERT}) (co-located with {DATE})}, year = {2013}, abstract = {The current trends in embedded systems are driving the integration of more functions in one processing element. At the same time, multicore architectures are increasingly used to improve performance, reduce costs, power consumption and size. Safety-critical applications are developed according to certification standards, which, depending on the criticality level, dictate the development processes and certification procedures that have to be followed. Functions of different criticalities have to be separated, both temporally and spatially, otherwise a low-criticality function can corrupt a high-criticality function. Separation is difficult to achieve in multicores, which leads to very high certification costs: all the functions on a multicore have to be developed as if they are of highest criticality. The RECOMP (Reduced certification cost for trusted multicore platforms) project aims at reducing the certification costs of mixed-criticality applications on multicore platforms, and addresses several industries, including industrial automation, automotive and avionics. The reduction in certification costs is achieved through (1) the use of separation solutions among mixed-criticality functions, through a combination of communication infrastructure, hardware, operating systems and middleware, methods and tools and component models, such that the required independence is achieved; (2) reducing the need for tool qualification, which is very expensive, by performing a tool-chain analysis of the tools used to develop a particular system; (3) methods and tools which reduce development costs and assist the designers in the certification lifecycle. This paper presents the RECOMP approach to safety-critical multicore systems, with a focus on methods and tools.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://past.date-conference.com/date13/conference/workshop-w8}, } @inproceedings{TMR2013, author = {Teufl, Sabine and Mou, Dongyue and Ratiu, Daniel}, title = {MIRA: A Tooling-Framework to Experiment with Model-Based Requirements Engineering}, booktitle = {Proceedings of the 21st IEEE International Requirements Engineering Conference (RE)}, year = {2013}, timestamp = 2013.05.31, owner = {teufl}, abstract = {Model-based requirements engineering supports eliciting, specifying and analyzing the work products elaborated during the requirements engineering process by providing adequate models. However, especially the inclusion of formal models needs to be investigated further. These models represent requirements and have to be integrated with reference models that define and structure the work results and their relations. We have developed the research tool MIRA to provide an infrastructure for the tool-based evaluation of the usage of models in the field of requirements engineering. In this paper we present the research questions addressed by MIRA concerning the reference model and the formal models. We explain how MIRA supports answering these research questions.}, doi = {10.1109/RE.2013.6636740}, keywords = {AutoFOCUS3, MIRA, model-based requirements engineering, model-based systems engineering, MbSE}, } @inproceedings{MK_SE_2013, author = {Khalil, Maged}, title = {Pattern-Based Methods for Model-Based Safety-Critical Software Architecture Design: A PhD Thesis Proposal}, booktitle = {Software Engineering (Workshops)}, pages = {493--499}, year = {2013}, abstract = {Software-intensive systems that perform safety-critical tasks are increasingly prevalent and pervasive in today's world. Driven by the incessant increase in the number of integrated control units, communication systems and software, managing architectural complexity, let alone mastering it, is becoming an increasingly difficult task. Safety standards recommend (if not dictate) performing many analyses during the concept phase of development as well as the early adoption of multiple measures at the architectural design level, most of which has become part of the day-today business of safety-critical development, yet has to receive adequate tool support. This is particularly true if one wishes to front-load these aspects into an integrated solution environment, in which these (mostly) repetitive tasks can be automated. Model-based development techniques are increasingly used and well suited for these parameters. Combining argumentation logic used for safety cases and safety concepts with abstract reasoning using model-based system description I argue about architectural optimization for safety-critical development. My approach allows reasoning about the system through the use of compositional description, which integrates physical environment models with system functional description models, and links problem-solving patterns with component model libraries which include nominal as well as faulty behavior.}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://dl.gi.de/handle/20.500.12116/17401}, } @inproceedings{, author = {Voss, Sebastian and Sch{\"{a}}tz, Bernhard and Khalil, Maged and C{\^{a}}rlan, Carmen}, title = {Towards Modular Certification using Integrated Model-Based Safety Cases}, booktitle = {Proceedings of the International Workshop on Verification and Assurance ({VeriSure} 2013) (co-located with {CAV})}, publisher = {Springer}, year = {2013}, abstract = {Software-intensive systems are characterized by an increasing number of features implementing complex functionalities. In many domains, these new functionalities perform more and more safety-critical tasks. To argue about the safety of such systems, Safety Cases are a proven technique that allows a systematic argumentation. Safety Cases may contain complex arguments that can be decomposed corresponding to modular system artifacts. This paper illustrates how a model-based system design can be tightly integrated with safety case arguments, to demonstrate both how safety cases link safety-specific analysis techniques like FMEA or FTA to architectural elements to provide evidence for safety argumentation, as well as how safety cases can be directly applied to efficiently guide the construction of the system architecture w.r.t. the claims given in the safety case. We demonstrate how existing information about the system and tool assisted techniques (e.g. formal verification, statistical testing) can be integrated into a safety case for a convincing argument in a seamless model-based development environment.}, keywords = {Modular Certification, Safety Cases, Model-based Development, AutoFOCUS3, model-based safety cases, ExplicitCase, model-based systems engineering, MbSE}, url = {http://fm.csl.sri.com/VeriSure2013/}, } @inproceedings{Blech2012, author = {Blech, Jan Olaf and Falcone, Yli{\`{e}}s and Becker, Klaus}, title = {Towards Certified Runtime Verification}, booktitle = {Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM 2012)}, publisher = {ACM}, year = {2012}, month = nov, timestamp = 2013.07.23, owner = {jeraj}, address = {Kyoto, Japan}, abstract = {Runtime verification (RV) is a successful technique to monitor system behavior at runtime and potentially take compensating actions in case of deviation from a specification. For the usage in safety critical systems the question of reliability of RV components arises since in existing approaches RV components are not verified and may themselves be erroneous. In this paper, we present work towards a framework for certified RV components. We present a solution for implementations of transition functions of RV monitors and prove them correct using the Coq proof assistant. We extract certified executable OCaml code and use it inside RV monitors. We investigate an application scenario in the domain of automotive embedded systems and present performance evaluation for some monitored properties.}, doi = {10.1007/978-3-642-34281-3_34}, keywords = {Model-based Systems Engineering, MbSE}, } @inproceedings{, author = {Mou, Dongyue and Ratiu, Daniel}, title = {Binding requirements and component architecture by using model-based test-driven development}, booktitle = {2012 First IEEE International Workshop on the Twin Peaks of Requirements and Architecture (TwinPeaks)}, pages = {27--30}, year = {2012}, month = sep, abstract = {Model-based testing is a well known technique to generate automatically highly qualitative tests for a given system based on a simplified testing model. Test-driven development is an established development practice in the agile development projects, which implies firstly the partial specification of a system by using tests, and after this, the development of the system. In test driven development the system implementation is continuously checked against the tests in order to assess its correctness with respect to the specification. In this paper we investigate how can these two methods be combined such that the advantages of these two approaches can be leveraged: highly qualitative test-cases used as specification of requirements and support of a continuous checking of architecture. We propose to formalize sub-sets of requirements into models that are amenable to generate tests by using automatic techniques well-known from model based testing. These tests can then be used to check the system architecture specification against the requirements in a continuous manner.}, doi = {10.1109/TwinPeaks.2012.6344557}, keywords = {automatic programming, formal specification, object-oriented programming, program testing, program verification, software architecture, software prototyping, AutoFOCUS3, MIRA, model-based requirements engineering, model-based systems engineering, MbSE}, } @inproceedings{Huang2012, author = {Huang, Kai and Chen, Gang and Keddis, Nadine and Geisinger, Michael and Buckl, Christian}, title = {Demo Abstract: An Inverted Pendulum demonstrator for Timed Model-based Design of Embedded Systems}, booktitle = {2012 IEEE/ACM Third International Conference on Cyber-Physical Systems (ICCPS)}, pages = {224}, year = {2012}, month = apr, doi = {10.1109/ICCPS.2012.45}, keywords = {chromosome, embedded systems, field programmable gate arrays, FPGA platform, inverted pendulum demonstrator, middleware, model-based software design, modular software framework, nonlinear systems, pendulums, safety-critical embedded systems, safety-critical software, timed model-based design}, } @inproceedings{, author = {Blech, Jan Olaf and Mou, Dongyue and Ratiu, Daniel}, title = {Reusing Test-Cases on Different Levels of Abstraction in a Model Based Development Tool}, booktitle = {Proceedings 7th Workshop on Model-Based Testing ({MBT})}, series = {{EPTCS}}, pages = {13--27}, year = {2012}, month = mar, timestamp = 2012.03.25, address = {Tallinn, Estonia}, abstract = {Seamless model based development aims to use models during all phases of the development process of a system. During the development process in a component-based approach, components of a system are described at qualitatively differing abstraction levels: during requirements engineering component models are rather abstract high-level and underspecified, while during implementation the component models are rather concrete and fully specified in order to enable code generation. An important issue that arises is assuring that the concrete models correspond to abstract models. In this paper, we propose a method to assure that concrete models for system components refine more abstract models for the same components. In particular we advocate a framework for reusing testcases at different abstraction levels. Our approach, even if it cannot completely prove the refinement, can be used to ensure confidence in the development process. In particular we are targeting the refinement of requirements which are represented as very abstract models. Besides a formal model of our approach, we discuss our experiences with the development of an Adaptive Cruise Control (ACC) system in a model driven development process. This uses extensions which we implemented for our model-based development tool and which are briefly presented in this paper.}, doi = {10.4204/EPTCS.80.2}, keywords = {AutoFOCUS3, model-based testing, model-based systems engineering, MbSE}, } @inproceedings{, author = {Voss, Sebastian and Sch{\"{a}}tz, Bernhard}, title = {Scheduling shared memory multicore architectures in {AutoFOCUS3} using Satisfiability Modulo Theories}, booktitle = {{Tagungsband - Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme VIII, MBEES 2012}}, year = {2012}, month = feb, abstract = {This paper presents an approach to task and message scheduling for multicore architectures using a shared memory. A shared memory architecture is used in most of the current multicore systems. The presented approach is integrated in the AUTOFOCUS 3 toolchain that allows to automatically compute schedules for this architecture to fulfill certain system requirements. AUTOFOCUS 3 models are based on a formally defined system model using explicit data-flow and discrete-time semantics. Our approach relies on a symbolic encoding scheme, based on a scheduling model, that we generate out of AUTOFO-CUS 3 system architectures. This encoding scheme relies on the AUTOFOCUS 3 semantics of strong-and weak-causal com-ponents and enables to generate schedules, that fulfill certain system properties. In this paper we focus on finding optimized schedules with respect to the global discrete time base. This paper provides a formalization that describes the scheduling problem as a satisfiability problem using boolean formulas and linear arithmetical constraints. A state-of-the-art satisfiability modulo theories (SMT) solver is then used to compute these schedules. This paper demonstrates that state-of-the art satisfiability modulo theories solver can be used to to compute a schedule that fulfills certain system requirements and meet the challenges of providing both a convenient modeling language and the performance to solve industrialized-sized design problems.}, keywords = {AutoFOCUS3, design-space exploration, DSE, scheduling, model-based systems engineering, MbSE}, url = {http://www.in.tu-clausthal.de/fileadmin/homes/GI/Documents/MBEES12Proceedings.pdf}, } @inproceedings{Sommer2012a, author = {Becker, Klaus and Buckl, Christian and Camek, Alexander and Falk, Reiner and Fiege, Ludger and Gessner, J{\"{u}}rgen and Sommer, Stephan}, title = {{SW-basierte Integration von neuen Fahrzeugfunktionen in zentralisierten Controllern}}, booktitle = {Automotive - Safety & Security}, year = {2012}, abstract = {In aktuellen Fahrzeugen wird ein wesentlicher Teil der Fahrzeugfunktionen durch Software realisiert. Die Integration aktiv eingreifender Assistenzsysteme wird diesen Trend noch verst{\"{a}}rken und die Komplexit{\"{a}}t des Bordnetzes wird weiter zunehmen. In diesem Artikel stellen wir einen Ansatz vor, Bordnetz und Software im Fahrzeug {\"{u}}ber eine datenzentrische Middleware zu entkoppeln. Sie koordiniert die Kommunikation zwischen Funktionen, Sensorik und Aktorik zur Laufzeit. Basierende auf einer Zentralrechnerarchitektur wird eine redundante Datenbasis zur Verf{\"{u}}gung gestellt, die eine fail-operational Ausf{\"{u}}hrung auch von sicherheitskritischen Funktionen erlaubt. Wir stellen am Beispiel Plug-and-Play (PnP) eine neue Sekund{\"{a}}rfunktion vor, die durch diesen Ansatz erm{\"{o}}glicht wird. Safetyund Security-Aspekte der vorgestellten Architektur werden ebenfalls betrachtet.}, isbn = {978-3-88579-604-6}, keywords = {Model-based Systems Engineering, MbSE}, url = {https://dl.gi.de/handle/20.500.12116/17552}, } @inproceedings{Weissmann2011, author = {Wei{\ss}mann, Markus and Bedenk, Stefan and Buckl, Christian and Knoll, Alois}, title = {{Model Checking Industrial Robot Systems}}, booktitle = {Proceedings of the 18th International Workshop on Model Checking of Software (SPIN 2011)}, publisher = {Springer-Verlag}, series = {LNCS}, pages = {161--176}, year = {2011}, month = jul, owner = {weissmam}, doi = {10.1007/978-3-642-22306-8_11}, keywords = {abstract interpretation, distributed systems, industrial robots, model checking, robotics}, url = {Weissmann2011.pdf}, } @techreport{, author = {Feilkas, Martin and H{\"{o}}lzl, Florian and Pfaller, Christian and Rittmann, Sabine and Sch{\"{a}}tz, Bernhard and Schwitzer, Wolfgang and Sitou, Wassiou and Spichkova, Maria and Trachtenherz, David}, title = {A Refined Top-Down Methodology for the Development of Automotive Software Systems - The Keyless Entry-System Case Study}, year = {2011}, month = feb, timestamp = 2011.02.11, school = {Technische Universit{\"{a}}t M{\"{u}}nchen}, abstract = {This technical report advances the methodology for the model-based development of automotive systems that was already defined in [FFH + 09], which was evaluated by developing an Adaptive Cruise Control (ACC) system with Pre-Crash Safety (PCS) functionality.}, keywords = {AutoFOCUS3, model-based testing, case study, model-based systems engineering, MbSE}, url = {https://mediatum.ub.tum.de/1094230}, } @inproceedings{TKM+2011, author = {Teufl, Sabine and Khalil, Maged and Mou, Dongyue and Geisberger, Eva}, title = {Experience with content-based requirements engineering assessments}, booktitle = {Proceedings of the 19th International Requirements Engineering Conference}, publisher = {IEEE}, pages = {345-346}, year = {2011}, abstract = {Identifying strengths and weaknesses in requirements engineering (RE) activities and deriving corresponding improvement and rectification recommendations are the main goals of the presented content-based RE assessment approach, which relies on a well-founded RE reference model. Two representative examples from our case study pool, carried out for companies with established RE practices in different domains, demonstrate the approach, its results and benefits.}, doi = {10.1109/re.2011.6051668}, keywords = {Model-based Systems Engineering, MbSE}, crossref = {DBLP:conf/re/2011}, } @inproceedings{, author = {Campetelli, Alarico and H{\"{o}}lzl, Florian and Neubeck, Florian}, title = {User-friendly Model Checking Integration in Model-based Development}, booktitle = {Proceedings of the 24th International Conference on Computer Applications in Industry and Engineering}, year = {2011}, abstract = {We present our approach to a user-friendly model checking integration in model-based development. The used modeling tool is AutoFocus 3, developed at our research group and specialized for reactive and embedded systems. For this integration, we approach usability at four points: tight coupling of verification properties with model elements, different specification languages for the formulation of properties, visualization of counterexamples as well as evaluation of different model checkers for adequate performance. Dealing with these issues leads to one of the first model-based development environments incorporating property specification, model checking and debugging.}, keywords = {verification, model checking, model-based development, tool support, embedded systems, AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, } @techreport{, author = {H{\"{o}}lzl, Florian and Spichkova, Maria and Trachtenherz, David}, title = {AutoFocus Tool Chain}, number = {TUM-I1021}, year = {2010}, month = nov, school = {Technische Universit{\"{a}}t M{\"{u}}nchen}, abstract = {This work presents the tool support for a model-based development methodology for verified software systems. We focus in this discussion on the design, implementation and the verification phase of the overall methodology developed for safety-critical embedded systems. In particular, we show how design models are transformed into C code and Isabelle/HOL theories by code generators. We discuss the applied AutoFocus tool chain and its basic principles emphasizing the verification of the system under development as well as the check mechanisms we applied to raise the level of confidence in the correctness of the implementation of the automatic generators.}, keywords = {AutoFOCUS3, methodology, tooling, model-based systems engineering, MbSE, architecture, verification}, url = {https://mediatum.ub.tum.de/1094431}, } @inproceedings{Buckl2010c, author = {Buckl, Christian and Gaponova, Irina and Geisinger, Michael and Knoll, Alois and Lee, Edward A.}, title = {Model-Based Specification of Timing Requirements}, booktitle = {Proceedings of the 10th ACM International Conference on Embedded Software (EMSOFT 2010)}, publisher = {Association for Computer Machinery}, pages = {239--248}, year = {2010}, month = oct, institution = {Technische Universit{\"{a}}t M{\"{u}}nchen}, address = {Scottsdale, Arizona, USA}, abstract = {In the past, model-based development focused mainly on functional and structural aspects of thesystem to be developed. Recently, several approaches to include timing aspects have been suggested.However, these approaches focus predominantly on later development phases. Models specifyingthe requirements with respect to timing without focusing on a specific solution are missing.For example, few models allow the specification of the allowed jitter of a system.In this paper, we identify requirements that are necessary to express the desired timingbehavior of hard and soft real-time systems by analyzing different application domains.Based on these results, we evaluate existing approaches with respect to their suitabilityto model timing requirements and present an suitable approach. Finally, this paper describesthe application of the suggested approach in the context of an example from the automation domain.}, doi = {10.1145/1879021.1879053}, keywords = {Automation, embedded, Model-based Development, multifunk, Real-Time Systems, Requirements Analysis, Survey, time, Timing Requirements}, url = {Buckl2010c.pdf}, } @incollection{, author = {H{\"{o}}lzl, Florian and Feilkas, Martin}, title = {{AutoFOCUS}3 - A Scientific Tool Prototype for Model-Based Development of Component-Based, Reactive, Distributed Systems}, booktitle = {Model-Based Engineering of Embedded Real-Time Systems}, publisher = {Springer}, series = {LNCS}, volume = {6100}, year = {2010}, address = {Berlin Heidelberg}, abstract = {We give an introduction of the AutoFOCUS3 tool, which allows component-based modeling of reactive, distributed systems and provides validation and verification mechanisms for these models. Furthermore, AutoFOCUS3 includes descriptions of specific technical platforms and deployments. The modeling language is based on precise semantics including the notion of time and allows for a refinement-based methodology for the development of reactive systems, typically found in user-accessible embedded realtime-systems.}, doi = {10.1007/978-3-642-16277-0_13}, keywords = {AutoFOCUS3, methodology, tooling, model-based systems engineering, MbSE}, } @inproceedings{Barner2010a, author = {Barner, Simon and Geisinger, Michael and Huang, Jia and Knoll, Alois and B{\"{o}}nicke, Holger and Ament, Christoph and Mades, Jochen and Pittschellis, Reinhard and Bauer, Gerd}, editor = {Gausemeier, J{\"{u}}rgen and Ramming, Franz and Sch{\"{a}}fer, Wilhelm and Tr{\"{a}}chtler, Ansgar}, title = {{E}asy{K}it - {E}ine allgemeine {M}ethodik f{\"{u}}r die {E}ntwicklung von {S}teuerungskomponenten}, booktitle = {{E}ntwurf mechatronischer {S}ysteme}, series = {{HNI-Verlagsschriftenreihe}}, volume = {272}, pages = {23--36}, year = {2010}, institution = {Technische Universit{\"{a}}t M{\"{u}}nchen}, address = {Paderborn, Germany}, abstract = {Bei der Entwicklung mechatronischer Systeme spielen Entwurf und Implementierung der Steuerungskomponente eine entscheidende Rolle. Hierbei lassen sich die folgenden Trends feststellen: Zentralisierte, oft SPS-basierte Systeme werden vermehrt durch dezentrale Ans{\"{a}}tze abgel{\"{o}}st, bei denen die prozessnahe Vorverarbeitung von Sensorsignalen und die Erzeugung von Steuersignalen f{\"{u}}r die Aktorik von effizienten, auf die jeweilige Aufgabe spezialisierten Systemen {\"{u}}bernommen werden. Des Weiteren gibt es vermehrt Anstrengungen, die sequenzielle Entwicklung von Maschine, Steuerung und Software aufzubrechen und zu parallelisieren (Hardware/Software Co-Design). Die EasyKit-Methodik ist ein m{\"{o}}glicher Ansatz, um diesen Anforderungen gerecht zu werden: Mit einem Elektronik-Baukastensystem steht ein Mittel zur Verf{\"{u}}gung, mit dem sich effizient auf die vorliegende Aufgabe zugeschnittene Mikrocontroller-basierte Steuerungen entwickeln lassen, die ohne weitere Beschaltung g{\"{a}}ngige industrielle Signaltypen verarbeiten und in bestehende Bussysteme und Netzwerke integriert werden k{\"{o}}nnen. Die Entwicklung der Software erfolgt mit dem modellgetriebenen Werkzeug EasyLab auf hohem Abstraktionsniveau und unabh{\"{a}}ngig von der verwendeten Hardware-Architektur. Die Modellierung dient als Grundlage f{\"{u}}r einen vorlagenbasierten Code-Generator sowie eine Simulationskomponente, die den Entwickler bei Planung und Fehlersuche unterst{\"{u}}tzt. Dar{\"{u}}ber hinaus erlaubt es eine Debugging-Schnittstelle, Programme, die auf der Zielhardware ablaufen, in Echtzeit zu beobachten und zu manipulieren. Die universelle Einsetzbarkeit eines Entwicklungsprozesses spielt eine wichtige Rolle f{\"{u}}r dessen Akzeptanz. Daher zeigen wir anhand von drei Fallbeispielen auf, wie EasyKit verwendet werden kann, um sowohl die Entwicklung komplexer industrieller Systeme zu strukturieren als auch die entsprechenden Grundlagen in der Ausbildung anschaulich zu vermitteln.}, keywords = {Code Generation, components, didactics, easykit, EasyLab, embedded, model driven development, systems}, } @article{Broy2010, author = {Broy, Manfred and Feilkas, Martin and Herrmannsd{\"{o}}rfer, Markus and Merenda, Stefano and Ratiu, Daniel}, editor = {Balsamo, MariaSimonetta and Knottenbelt, William J. and Marin, Andrea}, title = {Seamless Model-Based Development: From Isolated Tools to Integrated Model Engineering Environments}, journal = {Proceedings of the IEEE}, volume = {98}, pages = {526 - 545}, year = {2010}, timestamp = 2013.08.20, owner = {jeraj}, abstract = {More than 20 years of research has created a large body of ideas, concepts, and theories for model-based development of embedded software-intensive systems. These approaches have been implemented by several tools and successfully applied to various development projects. However, the everyday use of model-based approaches in the automotive and avionic industries is still limited. Most of the time, the engineers work with a predefined set of isolated tools, and therefore adapt their engineering methods and process to the available tools. Today, the industry achieves tool integration by demand-driven, pragmatic, and ad-hoc composed chains of a priori existent commercial tools. Nevertheless, these tool chains are not (and cannot be) seamless, since the integration that can be achieved is not deep enough. This hampers the reuse and refinement of models, which subsequently leads to problems like redundancy, inconsistency, and lack of automation. In the end, these deficiencies decrease both the productivity and quality that could be provided by model-based approaches. To overcome these problems, a deep, coherent, and comprehensive integration of models and tools is required. Such an integration can be achieved by the following three ingredients: 1) a comprehensive modeling theory that serves as a semantic domain for the models, 2) an integrated architectural model that holistically describes the product and process, and 3) a manner to build tools that conform to the modeling theory and allow the authoring of the product model. We show that from a scientific point of view, all ingredients are at our hands to do a substantial step into an integrated process and tool world. Further, we illustrate why such a solution has not been achieved so far, and discuss what is to be done to get a step closer to seamless model-based engineering.}, doi = {10.1109/JPROC.2009.2037771}, keywords = {AutoFOCUS3, methodology, tooling, model-based systems engineering, MbSE}, }