Philipp Chrszon

During the design of systems, engineers collaborate across disciplines with the aim of identifying a suitable design that matches their expectations. Such design is composed of a group of components, called a configuration. A configuration is Pareto-optimal if there is no other configuration that improves at least one objective without worsening another. Identifying such configurations is often performed using processes that are separated from one another. This costs time and is error prone during their integration. Despite contributions in this field, engineers are still provided with Pareto-optimal configurations but no means of analyzing their impact across coupled subsystems. It remains difficult for engineers to decide which configuration to select for their design. Moreover, tradeoff analysis that enables the evaluation of alternative configurations is usually performed using separate tools. This increases the burdens for engineers who understand the changes across subsystems, but have to evaluate these changes to find an optimal configuration. To address these challenges, this paper presents Change Impact Analysis Tradeoff (CIAT), an approach that identifies and analyzes configurations dynamically. To achieve this, it integrates knowledge graphs with change propagation, impact analysis, and tradeoff analysis in a single process. These capabilities favor dynamic analysis of configurations that can later be used by a digital twin to support design decisions. The proposed approach is currently illustrated in the context of space system design.

Ensuring the correct and safe behavior of a spacecraft is a main objective in space-system design. Since spacecraft consist of highly complex and tightly integrated components developed by large teams of engineers from various different disciplines, this is a challenging task. Increasingly, formal verification methods such as model checking are applied to establish the correctness of safety-critical parts or subsystems. Generally, the often limited scalability of model checking due to the state-space explosion problem hinders the wide-spread adoption of this technique. In this paper, we systematically examine the scalability of model checking for verifying behavioral models that arise within early space-system design phases. For this, we created a representative model for the mode management of a satellite that can be scaled in terms of its size and the complexity of interactions between system components. The model can be transformed into the input languages of various model-checking tools, which enables a comparative study of various model-checking algorithms and also facilitates analyzing the impact of different communication schemes on the scalability. The evaluation shows promising results regarding the applicability of model checking within the spacecraft design process.

The concept of features provides an elegant way to specify families of systems. Given a base system, features encapsulate additional functionalities that can be activated or deactivated to enhance or restrict the base system’s behaviors. Features can also facilitate the analysis of families of systems by exploiting commonalities of the family members and performing an all-in-one analysis, where all systems of the family are analyzed at once on a single family model instead of one-by-one. Most prominent, the concept of features has been successfully applied to describe and analyze (software) product lines. We present the toolProFeatthat supports the feature-oriented engineering process for stochastic systems by probabilistic model checking. To describe families of stochastic systems,ProFeatextends models for the prominent probabilistic model checkerPrismby feature-oriented concepts, including support for probabilistic product lines with dynamic feature switches, multi-features and feature attributes.ProFeatprovides a compact symbolic representation of the analysis results for each family member obtained byPrismto support, e.g., model repair or refinement during feature-oriented development. By means of several case studies we show howProFeateases family-based quantitative analysis and compare one-by-one and all-in-one analysis approaches.

Software systems in domains like Smart Cities, the Internet of Things or autonomous cars are coined by a high degree of distribution across several independent computing devices and the requirement to be able to adjust themselves to varying situations in their operational environment. Self-adaptive software systems are a natural choice to implement such context-dependent software systems. A multitude of approaches already implement self-adaptive systems and some consider even distribution aspects.Yet, none of the existing solutions supports the coordination of adaptation operations spanning multiple independent nodes, which is necessary to ensure a consistent adaptation even in presence of network errors or node failures. In this paper, we tackle this challenge to execute adaptations in distributed self-adaptive software systems in a coordinated manner. We present a protocol that enables the self-adaptive software system to execute correlated adaptations on multiple nodes in a transactional manner ensuring an atomic and consistent transition of the distributed system from its source to the desired target configuration. The protocol is validated to be free of deadlocks for any given adaptation at any point in time using a model-checking approach. The performance of our approach is investigated in experiments that emulate the protocol's execution on real devices for different sizes of distributed applications and adaptation scenarios.