@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}, } @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 = {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}, } @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}, } @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}, } @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 = {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}, } @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}, } @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{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}, } @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 = {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 = {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{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{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}, } @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{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{, 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}, }