Due to the impressive performance of deep neural networks (DNNs) for visual perception, there is an increased demand for their use in automated systems. However, to use deep neural networks in practice, novel approaches are needed, e.g., for testing. In this work, we focus on the question of how to test deep learning-based visual perception functions for automated driving. Classical approaches for testing are not sufficient: A purely statistical approach based on a dataset split is not enough, as testing needs to address various purposes and not only average case performance. Additionally, a complete specification is elusive due to the complexity of the perception task in the open context of automated driving. In this article, we review and discuss existing work on testing DNNs for visual perception with a special focus on automated driving for test input and test oracle generation as well as test adequacy. We conclude that testing of DNNs in this domain requires several diverse test sets. We show how such tests sets can be constructed based on the presented approaches addressing different purposes based on the presented methods and identify open research questions.

Cyber-physical systems reconfigure the structure of their software architecture, e.g., to avoid hazardous situations and to optimize operational conditions like their energy consumption. These reconfigurations have to be safe so that the systems protect their users or environment against harmful conditions or events while changing their structure. As software architectures are typically built on components, reconfiguration actions need to take into account the component structure. This structure should support vertical composition to enable hierarchically encapsulated components. While many reconfiguration approaches for cyber-physical and embedded real-time systems allow the use of hierarchically embedded components, i.e., vertical composition, none of them offers a modeling and verification solution to take hierarchical composition, i.e., encapsulation, into account thus limiting reuse and compositional verification. In this paper, we present an extension to our existing modeling language, MechatronicUML, to enable safe hierarchical reconfigurations. The three extensions are (a) an adapted variant of the 2-phase-commit protocol to initiate reconfigurations that maintain component encapsulation, (b) the integration of feedback controllers during reconfiguration, and (c) a verification approach based on (timed) model checking for instances of our model. We illustrate our approach on a case study in the area of smart railway systems by showing two different use cases of our approach. We show that using our approach the systems can be easily designed to reconfigure safely.

Today’s mechatronic systems are increasingly interconnected using communication protocols for realizing advanced functionality. Communication protocols underlie hard real-time constraints and need to meet high quality standards for ensuring the safety of the system. A common approach for achieving their necessary quality and mastering their impending complexity is model-driven development. Applying this approach, a developer builds formal models of the communication protocols and applies formal verification techniques (e.g., model checking) for proving that the communication is safe. However, these techniques typically face the state-explosion problem that prevents proofs for large systems like interconnected mechatronic systems. In previous publications, we introduced the MechatronicUML method that provides a compositional verification approach for tackling the state-explosion problem. A key enabler for such an approach is a definition of refinement. In this paper, we extend the compositional verification approach of MechatronicUML in particular by using different kinds of refinement definitions including an automatic selection of the most suitable refinement definition. In addition, we significantly extend an existing approach of test automata construction for refinement checking. Using this approach we can also guarantee that a refined model is constructed correctly concerning the selected and applied refinement definition. We evaluate our approach by an example of an advanced railway transportation system.

Current and especially future software systems increasingly exhibit so-called self-* properties (e.g., self-healing or self-optimization). In essence, this means that software in such systems needs to be reconfigurable at run-time to remedy a detected failure or to adjust to a changing environment. Reconfiguration includes adding or deleting (software) components as well as adding or deleting component interaction. As a consequence, the state space of self-* systems becomes so complex, that current verification approaches like model checking or theorem proving usually do not scale. Our approach addresses this problem by firstly defining a system architecture with clearly defined components and their interfaces (ports including the definition of signatures of all events and methods which the port may receive and the component may execute) and so-called coordination patterns. These coordination patterns specify communication protocols based on the definition of the ports only for those component interactions which are defined in the (static) architecture specification by a corresponding connection. Secondly, the reconfiguration of architectures is precisely defined by giving a formal definition of all change operations, e.g., adding or deleting components and component connections. By exploiting this formal definition, it becomes provable that an architecture includes only component connections which correspond to the defined coordination patterns. Then, the verification of safety and liveness properties has to be carried out only for each individual coordination pattern rather than for the system as a whole.

Threat metrics are used to measure the criticality of traffic situations. Such metrics rely on models predicting future behavior of other traffic participants. These models need to be calculated with respect to lanes for handling oncoming traffic, but in urban scenarios, lanes are often not explicitly defined. In this paper, we present a first modeling and conformance testing approach for criticality metrics in urban scenarios. In addition, we analyze the influence of lane association on the quality of the models used for threat prediction. We evaluate our approach based on an urban intersection from the inD dataset. Our key finding is that such metrics are in general prone to both false positives and negatives if maps with static lanes are used.

The evaluation of camera-based perception functions in automated driving (AD) is a significant challenge and requires large-scale high-quality datasets. Recently proposed metrics for safety evaluation additionally require detailed per-instance annotations of dynamic properties such as distance and velocities that may not be available in openly accessible AD datasets. Synthetic data from 3D simulators like CARLA may provide a solution to this problem as labeled data can be produced in a structured manner. However, CARLA currently lacks instance segmentation ground truth. In this paper, we present a back projection pipeline that allows us to obtain accurate instance segmentation maps for CARLA, which is necessary for precise per-instance ground truth information. Our evaluation results show that per-pedestrian depth aggregation obtained from our instance segmentation is more precise than previously available approximations based on bounding boxes especially in the context of crowded scenes in urban automated driving.

Whenever a visual perception system is employed in safety-critical applications such as automated driving, a thorough, task-oriented experimental evaluation is necessary to guarantee safe system behavior. While most standard evaluation methods in computer vision provide a good comparability on benchmarks, they tend to fall short on assessing the system performance that is actually relevant for the given task. In our work, we consider pedestrian detection as a highly relevant perception task, and we argue that standard measures such as Intersection over Union (IoU) give insufficient results, mainly because they are insensitive to important physical cues including distance, speed, and direction of motion. Therefore, we investigate so-called relevance metrics, where specific domain knowledge is exploited to obtain a task-oriented performance measure focusing on distance in this initial work. Our experimental setup is based on the CARLA simulator and allows a controlled evaluation of the impact of that domain knowledge. Our first results indicate a linear decrease of the IoU related to the pedestrians' distance, leading to the proposal of a first relevance metric that is also conditioned on the distance.

The use of neural networks in perception pipelines of autonomous systems such as autonomous driving is indispensable due to their outstanding performance. But, at the same time their complexity poses a challenge with respect to safety. An important question in this regard is how to substantiate test sufficiency for such a function. One approach from software testing literature is that of coverage metrics. Similar notions of coverage, called neuron coverage, have been proposed for deep neural networks and try to assess to what extent test input activates neurons in a network. Still, the correspondence between high neuron coverage and safety-related network qualities remains elusive. Potentially, a high coverage could imply sufficiency of test data. In this paper, we argue that the coverage metrics as discussed in the current literature do not satisfy these high expectations and present a line of experiments from the field of computer vision to prove this claim.

Scenario-based approaches have gained popularity in the context of automated vehicles. As in any model-based approach, validation to real data needs to be considered. This work studies concrete scenarios based on real data from a large-scale and open road user trajectory dataset. In particular, we detail on cut-ins and (hard) braking maneuvers and study them based on existing threat metrics. In this work, we present the complete workflow starting from the pre-processing and validation of the data, the definition of concrete scenarios based on how we extract them from the dataset and their evaluation based on several threat metrics. We identify peculiarities of the dataset itself, as well as of the driving behavior of vehicles therein. As this work relies on an open dataset, results can be reproduced and readily compared.

Highly automated driving systems need to master a highly complex environment and are required to show meaningful behavior in any situation occurring in mixed traffic with humans. Deriving a sufficiently complete and consistent set of system-level requirements capturing all possible traffic situations is a significant problem that has not been solved in existing literature. In this paper, we propose a new method called SOCA addressing this problem by introducing a novel abstraction of traffic situations, called zone graph, and using this abstraction in a morphological behavior analysis. The morphological behavior analysis enables us to derive a set of system-level requirements with guarantees on completeness and consistency. We illustrate our method on a slice-of-reality example from the automated driving domain.

Deep learning-based approaches have gained popularity for environment perception tasks such as semantic segmentation and object detection from images. However, the different nature of a data-driven deep neural nets (DNN) to conventional software is a challenge for practical software verification. In this work, we show how existing methods from software engineering provide benefits for the development of a DNN and in particular for dataset design and analysis. We show how combinatorial testing based on a domain model can be leveraged for generating test sets providing coverage guarantees with respect to important environmental features and their interaction. Additionally, we show how our approach can be used for growing a dataset, i.e. to identify where data is missing and should be collected next. We evaluate our approach on an internal use case and two public datasets.

Automated test generation and evaluation in simulation environments is a key technology for verification of automated driving (AD) applications. Search-based testing (SBT) is an approach for automated test generation that leverages optimization to efficiently generate interesting concrete tests from abstract test descriptions. In this experience paper, we report on our observations after successfully applying SBT to AD control applications in several use cases with different characteristics. Based on our experiences, we derive a number of lessons learned that we consider important for the adoption of SBT methods and tools in industrial settings. The key lesson is that SBT finds relevant errors and provides valuable feedback to the developers, but requires tool support for writing specifications.

Vision is an important sensing modality in automated driving. Deep learning-based approaches have gained popularity for different computer vision (CV) tasks such as semantic segmentation and object detection. However, the black-box nature of deep neural nets (DNN) is a challenge for practical software verification. With this paper, we want to initiate a discussion in the academic community about research questions w.r.t. software testing of DNNs for safety-critical CV tasks. To this end, we provide an overview of related work from various domains, including software testing, machine learning and computer vision and derive a set of open research questions to start discussion between the fields.

Preprogramming of tasks still plays an important role in complex robotic systems despite the advances in automated planning and symbolic learning. Often, it is desired that end-users implement further tasks to adapt the robotic application to their needs. These user-defined tasks have to meet safety and integrity constraints for protecting the robotic platform and its users. We introduce a verifiable task specification language (vTSL) that enables to automatically prove that a task specification satisfies a set of predefined or task-specific constraints. We illustrate our approach using an example of a self-driving vehicle for intra-logistics and report experiences with two commercial applications.

This paper describes the challenges involved in arguing the safety of highly automated driving functions which make use of machine learning techniques. An assurance case structure is used to highlight the systems engineering and validation considerations when applying machine learning methods for highly automated driving. Particular focus is placed on addressing functional insufficiencies in the perception functions based on convolutional neural networks and possible types of evidence that can be used to mitigate against such risks.

Mobile robots operating in a shared environment with pedestrians are required to move provably safe to avoid harming pedestrians. Current approaches like safety fields use conservative obstacle models for guaranteeing safety, which leads to degraded performance in populated environments. In this paper, we introduce an online verification approach that uses information about the current pedestrian velocities to compute possible occupancies based on a kinematic model of pedestrian motion. We demonstrate that our method reduces the need for stopping while retaining safety guarantees, and thus goals are reached between 1.4 and 3.5 times faster than the standard ROS navigation stack in the tested scenarios.

Machine learning technologies such as neural networks show great potential for enabling automated driving functions in an open world context, for example, for videobased object detection and classification or trajectory planning. However, these technologies can only be released for series production if they can be demonstrated to be sufficiently safe. Existing functional safety standards such as ISO 26262 do not transfer well to demonstrating the safety of machine learning and in particular regarding functional insufficiencies in open context systems. Therefore, convincing arguments need to be developed for the safety of automated driving systems based on such technologies. A structured assurance case, based on the Goal Structuring Notation (GSN) is introduced as a means for providing such an argument. By following the assurance case principles, it becomes clear that a systems engineering approach is required to derive a precise definition of the performance requirements on the function to be implemented on which to base the safety case. This includes an explicit formulation of assumptions and contextual information relevant to the specific application.

Real-time properties such as reaction times play a safety-critical role for service robot applications. Current robotic software frameworks and middlewares, however, abstract from the underlying executing platform and execution management of the operating system thereby hiding relevant timing information. In other domains, such as automotive, model-based timing analysis is used early in the development process to analyze timing properties of the system. These approaches are not yet common in the service robotics domain. In this paper, we extend a model-driven development approach for robotic systems and enhance the system-configuration step to include a novel performance view that enables model-based timing analysis for robotic applications. Our evaluation shows that the performance analysis reasonably represents the real robot's run-time performance.

The component-based software architecture of a cyber-physical system (CPS) is often subject to structural reconfigurations in response to changing environmental conditions. When introducing reconfigurations to CPS, it is mandatory to ensure that the execution of a reconfiguration does not compromise the safety of the system, e.g., by causing a violation of hard real-time constraints. Existing approaches for ensuring safe reconfiguration do not consider such hard realtime constraints or the interaction of a CPS with its physical environment. Thus, they can not detect all relevant unsafe situations. In this paper, we introduce a novel approach that is based on a design-time specification of conditions for unsafe states combined with a runtime evaluation of these conditions. This enables to detect all relevant unsafe states with respect to a requested reconfiguration at runtime. We illustrate our approach based on a smart railway system.

Cyber-physical systems (CPS) require model checking to guarantee the functional correctness of software models, providing counterexamples in case of violations. Domain-specific model checking (DSMC) allows to apply model checking to specific application domains. DSMC hides the complexity of using a model checker by translating from a domain-specific modeling language (DSML) to the model checker’s input language, and by translating counterexamples back to the domain-specific level. Implementing DSMC is challenging for CPS due to the large differences between DSMLs and the input language of a model checker. In this paper, we present a successful application of DSMC to MechatronicUML, a DSML for the software design of CPS, using the model checker Uppaal . As a key benefit, our approach is able to translate counterexamples back to the domain-specific level even in case of large differences between DSML and the model checker’s input language. We show the correctness of our approach using a case study from the area of car-2-car communication.

Cyber-physical systems, e.g., autonomous cars or trains, interact with their physical environment. As a consequence, they commonly have to coordinate with other systems via complex message communication while realizing safety-critical and real-time tasks. As a result, those systems should be correct by construction. Software architects can achieve this by using the MechatronicUML process and language. This paper presents the MechatronicUML Tool Suite that offers unique features to support the MechatronicUML modeling and analyses tasks.

This paper proposes a solution to the IMDb movie database case of the Transformation Tool Contest 2014. Our solution is based on the Eclipse implementation of the OMG standard QVTo. We implemented all of the tasks including all of the extension tasks. Our benchmark results show that QVTo is able to handle models with a few thousand objects.

The software of mechatronic systems interacts with the system's physical environment. In such systems, an incorrect software may cause harm to human life. As a consequence, software engineering methods for developing such software need to enable developers to effectively and efficiently proof their correctness. This is further complicated by additional characteristics of mechatronic systems as self-adaptation and coordination with other systems. In this poster, we present MechatronicUML which is a model-driven software engineering method that especially considers these characteristics of self-adaptive mechatronic systems.

Advanced mechatronic systems, like smart cars or smart trains, perform reconfiguration as a reaction to their changing environment. The reconfiguration behaviour of such systems is safety-critical and needs to be verified by formal verification procedures. In the past, graph transformation systems have proven to be a suitable formalism for specification and verification of such systems. However, existing approaches do not consider that reconfiguration operations consume time. Considering their duration, several reconfiguration operations can be executed concurrently in a running system, possibly resulting in undesired behaviour. In this paper, we introduce durations for graph transformation rules and a locking mechanism that ensures the safe concurrent execution of time-consuming operations. Additionally, we show how graph transformation rules with durations are mapped to an existing verification framework which enables the formal verification of graph transformation systems with durative rules. We illustrate our approach using an example of a smart train system.

Mechatronic systems reconfigure the structure of their software architecture, e.g., to avoid hazardous situations or to optimize operational conditions like minimizing their energy consumption. As software architectures are typically build on components, reconfiguration actions need to respect the component structure. This structure should be hierarchical to enable encapsulated components. While many reconfiguration approaches for embedded real-time systems allow the use of hierarchically embedded components, i.e., horizontal composition, none of them offers a modeling and verification solution to take hierarchical composition, i.e., encapsulation, into account. In this paper, we present an extension to our existing modeling language, \muml, to enable safe hierarchical reconfigurations. The two main extensions are (a) an adapted variant of the two-phase commit protocol to initiate reconfigurations which maintain component encapsulation and (b) a timed model checking verification approach for instances of our model. We illustrate our approach on a case study in the area of smart railway systems by showing two different use cases of our approach and the verification of their safety properties.

The automotive industry uses MATLAB/Simulink models for specifying the behavior of software components and for early validation of that behavior using model-in-the-loop simulations. During a simulation run, these models may not structurally change. Thus, MATLAB/Simulink is not amenable to realizing self-adaption behavior, where the software architecture of the system evolves during runtime. In this paper, we show how to model self-adaptive software using our language Mechatronic UML and how we transform a model specified in Mechatronic UML into a MATLAB/Simulink model automatically. In particular, we generate several helper functions that emulate self-adaptive behavior in MATLAB/Simulink, relying only on standard Simulink blocks. We illustrate our approach using an example of car platoons.

Embedded real-time systems are increasingly applied in safety-critical environments like cars or aircrafts. Even though the system design might be free from flaws, hazardous situations may still be caused at run-time by random faults due to the wear of physical components. Hazard analysis is based on fault trees or failure propagation models. These models are created at least partly manually. They are usually independent from the software models which are used for checking safety and liveness properties to avoid systematic faults. This is particularly bad in cases, where the software model contains manually specified operations to deal with random faults which have been identified by hazard analysis. These operations include replacing the faulty components by reconfiguration. We propose to generate a failure propagation model automatically from the software model to check whether the results of hazard analysis have been properly accounted in the specification of reconfiguration operations. In contrast to other approaches, our approach considers the real-time properties of the system and adds explicit failure propagation times based on using timed automata for model specification.

Technical systems contain mechanical, electrical, and software parts. Consequently, they are developed by engineers of the respective disciplines. However, current industrial practice as well as existing development processes do not account for the required tight integration between the engineers of the different disciplines. Processes become even more complex, when self-adaptive systems are built. In this paper, we present a development process for selfadaptive mechatronic systems which particularly addresses the integration between the disciplines concerned with the development of software, namely control and software engineering. We illustrate the process by presenting examples from the development of autonomous railway vehicles which build convoys to improve energy efficiency.

Model-driven development of real-time safety-critical systems requires to support refinement of behavioral model specifications using, for example, timed simulation or timed bisimulation. Such refinements, if defined properly, guarantee that (safety and liveness) properties, which have been verified for an abstract model, still hold for the refined model. In this paper, we propose an automatic selection algorithm selecting the most suitable refinement definition concerning the type of model specification applied and the properties to be verified. By extending the idea of test automata construction for refinement checking, our approach also guarantees that a refined model is constructed correctly concerning the selected and applied refinement definition. We illustrate the application of our approach by an example of an advanced railway transportation system.

Das Thema Elektromobilität hat in der Fahrzeugindustrie in den letzten Jahren viel Aufmerksamkeit erhalten. Gerade im Bereich der Entwicklung von Steuergeräte-Software ist der Bedarf an frühzeitiger Absicherung hoch. Nur so können Produkteinführungszeiten minimiert und effektiv Entwicklungskosten eingespart werden. Komplexe Werkzeugketten und die verteilte Entwicklung erschweren den Prozess und verlängern die Entwicklungszeit. Das Förderprojekt "Simulationsgestützter Entwurf für Elektrofahrzeuge", kurz "E-Mobil", nimmt sich der Herausforderungen einer verteilten Entwicklung von Steuergeräte-Software an. Vier Projektpartner aus Industrie und Forschung untersuchen die Besonderheiten sowohl bzgl. des Entwurfsprozesses, als auch der beteiligten Entwurfswerkzeuge im Vergleich zur konventionellen Fahrzeugentwicklung. Im Fokus stehen die Modellierung und die simulationsgestützte Absicherung in frühen Entwurfsstadien. Die Modellierung umfasst Regelungssoftware sowie die für die Simulation nötigen elektrischen und mechatronischen Komponenten. Die vorliegende Arbeit stellt die Kernthemen sowie aktuelle Ergebnisse aus dem Projekt vor.

In dieser Arbeit wird eine Methode für die Verifikation der Software von interagieren den mechatronischen Systemen vorgestellt, die sowohl das zeitkontinuierliche Verhalten als auch das ereignisdiskrete Verhalten dieser Systeme berücksichtigt. Dabei wird das zeitkontinuierliche Verhalten der mechatronischen Systeme durch sogenannte Profile abstrahiert, die dann für die Verifikation des diskreten Nachrichtenaustauschs ausgenutzt werden. Erst hierdurch wird das gesamt hybride System für eine Verifikationsmethode beherrschbar. Exemplarisch wird die modellbasierte Profilgenerierung anhand von Bremsprofilen für ein kontrolliertes Abbremsen eines Konvois von autonomen Schienenfahrzeugen, sogenannten RailCabs, vorgestellt. Sie basiert auf Verfahren der optimalen Steuerung unter Berücksichtigung verschiedener Zielkriterien. Es wird dann verifiziert, ob beim Einscheren eines neuen RailCabs in einen bestehenden Konvoi eine korrekte Bremsprofilverteilung garantiert werden kann.

Today's real-time embedded systems operate in frequently changing environments on which they react by self-adaptations. Such an approach needs adequate modeling support of these reconfigurations to enable verification of safety properties, e.g., by timed model checking. Component-based development of such systems realizes these self-adaptations by structural reconfigurations of components and their connectors. However, component models proposed in literature do not support reconfigurable components in real-time embedded context but focus on other domains like business information systems. In this paper, we present an extension of our modeling language MechatronicUML to support structural reconfigurations taking the specific requirements of our domain into account. Based on the proposed extension we outline our research roadmap to achieve verification and realization of systems modeled in MechatronicUML.

Today's real-time embedded systems operate in frequently changing environments on which they react by self-adaptations. Such an approach needs adequate modeling support of these reconfigurations to enable verification of safety properties, e.g., by timed model checking. Component-based development of such systems realizes these self-adaptations by structural reconfigurations of components and their connectors. However, component models proposed in literature do not support reconfigurable components in real-time embedded context but focus on other domains like business information systems. In this paper, we present an extension of our modeling language MechatronicUML to support structural reconfigurations taking the specific requirements of our domain into account. Based on the proposed extension we outline our research roadmap to achieve verification and realization of systems modeled in MechatronicUML.

Modern technical systems are increasingly built to exhibit self-x properties as, e.g., self-healing or self-optimization. For this, they require adaptation at runtime. This is even true for embedded or mechatronic systems which often operate in safety critical environments. There, the effects of theadaptation with respect to safety must be analyzed carefully. However, not all parameters needed for safety analyses, e.g., the concrete system architecture, are known at design time. Consequently, safety analyses need to be executed during runtime. Current approaches of runtime safety analysis typically react to anomalies that already occurred in the system. Thus, unsafe system states cannot be excluded completely. We present a runtime safety analysis that prevents system states with an unacceptable risk that have not yet occurred. For this, we generate the reachable component structures at runtime and analyze them with respect to risk. The system is modified such that component structures with an unacceptable risk are not reachable any more and are thus prevented.

Innovation in today’s mechanical systems is often only possible due to the embedded software. Particularly, the software connects previously isolated systems resulting in, so-called, advanced mechatronic systems. Mechatronic systems are often employed in a safety-critical context, where hazards that are caused by faults in the software have to be prevented. Preferably, this is achieved by already avoiding these faults during development. A major source of faults is the complex coordination between the connected mechatronic systems. In this paper, we present Real-Time Coordination Patterns for advanced mechatronic systems. These patterns formalize proven communication protocols for the coordination between mechatronic systems as reusable entities. Furthermore, our approach exploits the patterns in the decomposition of the system to enable a scalable formal verification for the detection of faults. We illustrate the patterns with examples from different case studies.

Component based software engineering aims at re-using components in other systems. This requires a verification whether the component can safely interact with its communication partners in a new environment. Such verification is mandatory in case of safetycritical real-time systems where the communication is characterized by a varying number of components instances all being of the same type. Reuse can be facilitated by separating abstract communication protocol definitions and concrete component implementations. In contrast to standard refinement definitions for real-time systems, our definition explicitly takes varying numbers of communication partners into account. Additionally, we relax the strict conditions of a bisimulation to ease reuse of components. Along with our refinement definition, we provide a formal verification procedure to check for correct refinements which preserves properties verified for the abstract protocol definition. We evaluated our approach using a self-adaptive real-time system from the domain of autonomous train systems. The evaluation results show that checking for correct refinements is more efficient than re-verifying the desired properties on the refined component.

Model-based software engineering aims at specifying the system under construction by abstract models that can be used for formal verification of the system behavior. In the case of real-time systems, such verification requires special algorithms dealing with time computations. These computations can be performed efficiently by using zone graphs [1, 3]. Current implementations, however, cannot be used in FUJABA. Therefore, we introduce a TCP/IP-based client/server architecture wrapping an existing implementation in a server such that it can be used by arbitrary clients. In our evaluation, we show that the TCP/IP overhead is negligible compared to the total run-time.

Story-driven modeling (SDM) is a model-based specification approach combining UML activity diagrams and graph transformations. In recent years, the development in the SDM community led to many incompatible meta-models for story diagrams based on the same common concepts. The diversity of meta-models hindered the reuse of tools and limited synergy effects. In this paper, we introduce the new meta-model for story diagrams which was created in joint effort of the SDM community. The new EMF-based model integrates the recent developments and paves the way for the interoperation of SDM tools with each other and with EMF-based tools.

In recent years, software increasingly exhibits self-* properties like selfoptimization or self-healing. Such properties require reconfiguration at runtime in order to react to changing environments or detected defects. A reconfiguration might add or delete components as well as it might change the communication topology of the system. Considering communication protocols between an arbitrary number of participants, reconfiguration and state-based protocol behavior are no longer independent from each other and need to be verified based on a common formalism. Additionally, such protocols often contain timing constraints to model real-time properties. These are of integral importance for the safety of the modeled system and thus need to be considered during the verification of the protocol. In current approaches either reconfigurations or timing constraints are not considered. Existing approaches for the verification of timed graph transformation systems lack important constructs needed for the verification of state-based real-time protocol behaviors. As a first step towards a solution to this problem, we introduced Timed Story Driven Modeling [HHH10] as a common formalism integrating state-based real-time protocol behaviors and system reconfigurations based on graph transformations. In this paper, we introduce a framework allowing to perform reachability analysis based on Timed Story Driven Modeling. The framework allows to compute the reachable timed graph transition system based on an initial graph and a set of timed transformation and invariant rules.

This paper addresses the topology analysis case study for the Transformation Tool Contest2010. The case study presents a car platoon merge protocol with a dynamic number of participants.The task is to compute a reachability graph for all system configurations generated by the graph rewriterules. Using the Fujaba Real-Time Tool Suite, we modeled the merge protocol as statechart in concretesyntax as this is more intuitive and use a special generator to derive the corresponding graph rewriterules ([6,5]). This has been combined with the hierarchical graphs library presented in [12], to computethe reachable graph transition system.

Software is increasingly used in systems which have to support self* properties like self-adaptation, -management or -optimization. The key enabler for a consistent model-based development approach is refinement. Refinement facilitates to preserve properties of abstract models in more concrete models. Note, that abstract models are of paramount importance to formal verification in complex safety critical systems. Despite the increased significance of self* properties in the last years, surprisingly there is a lack in support of refinement techniques being integrated in a model-based development approach. We present a modeling approach, called Timed Story Charts, which supports a exible specification of properties like self-adaptation, and furthermore, we will present an integrated refinement check.

Based on a well-defined component architecture the tool supports the synthesis of so-called real-time statecharts from timed sequence diagrams. The two step synthesis process addresses the existing scalability problems by a proper decomposition and allows the user to define particular restrictions on the resulting statecharts.

Whenever the growing amount of XML data that has to be stored, processed, exchanged, or transmitted becomes a major cost driver or performance bottleneck, XML compression is an important way to reduce these problems. However, many applications, e.g. those exchanging XML data streams, also require efficient path query processing on the structure of compressed XML data streams. We present an XML compression technique called DAG+BSBC, which extends Bit-Stream-Based-Compression (BSBC) [3] by a sparse index to compressed constants that reflects DAG pointers. Furthermore, DAG+BSBC supports XML stream compression, queries on compressed data, and provides a compression ra tio that not only significantly outperforms that of other queriable XML compression tech niques, like XGrind, but is also very competitive compared to non-queriable compression tech niques like gzip and XMill.

Automotive systems contain a large number of software controllers that interact in order to realize an increasing number of functions. The controllers are typically developed separately by different suppliers. Therefore, errors in the overall functionality are often detected late in the development process or even remain undetected. This affects the quality and safety of the systems and may lead to expensive recalls. We propose to specify the communication behavior more precisely in the early system design by modeling the controllers’ interactions using formal sequence diagrams (LSCs). Based on these behavior models we’re able to automatically synthesize state machines, which can be used to generate code for the communication behavior of the controllers. We provide a prototypical integrated modeling environment based on Fujaba which supports specifying requirements, modeling the component architecture, and component behavior as well as the state machine synthesis.

XML data compression is an important feature in XML data exchange, particularly when the data size may cause bottlenecks or when bandwidth and energy consumption limitations require reducing the amount of the exchanged XML data. However, applications based on XML data streams also require efficient path query processing on the structure of compressed XML data streams. We present a succinct representation of XML data streams, called Bit-Stream-Based-Compression (BSBC) that fulfills these requirements and additionally provides a compression ratio that is significantly better than that of other queriable XML compression techniques, ie XGrind and DTD subtraction, and that of non-queriable compression techniques like gzip. Finally, we present an empirical evaluation comparing BSBC with these compression techniques and with XMill that demonstrates the benefits of BSBC.

Self-adaptive mechatronic systems automatically adapt their behavior to a changing environment by reconfiguring their software architecture at runtime. In particular, this includes to dynamically form systems of systems at runtime, where several systems collaborate with each other using message-based communication protocols. Often, these systems are safety-critical and need to satisfy hard real-time constraints, i.e., any (timing) error in their behavior may put lives at risk. As a consequence, the software of a mechatronic system needs to meet high quality standards. In particular, it needs to be guaranteed that reconfigurations of the software architecture do not lead to an unsafe behavior or a violation of the real-time constraints. Testing alone cannot prove the correctness and thereby the safety of the mechatronic system. Existing approaches for model-driven development and analysis of mechatronic systems either provide support for analyzing real-time constraints or for analyzing reconfigurations of the software architecture, but none of the existing approaches supports both. In this thesis, we present a combination of constructive and analytical techniques that can be used by software engineers as part of a model-driven software engineering method for assuring the correctness of the software of a self-adaptive mechatronic system. As a key novelty, our approach combines formal verification and simulation-based testing for achieving a scalable analysis of the system's software. In addition, we explicitly separate the specification and verification of functional behavior and reconfiguration behavior for further improving the scalability of the verification. We evaluated all of our contributions based on the RailCab system and conducted two case studies that demonstrate the viability of our techniques.

Softwaresysteme unterliegen zunehmend Anforderungen wie Selbstadaption oder Selbstmanagement, d.h. die Systeme müssen sich an ihre veränderliche Umwelt anpas- sen. Die modellbasierte Entwicklung solcher Systeme wird erst durch die Definition ei- ner Verfeinerung möglich. Diese erlaubt es, eine Verifikation der relevanten Eigenschaf- ten auf abstrakten Modellen durchzuführen und diese dann schrittweise hin zu einer Implementierung zu verfeinern. Dabei müssen die relevanten, auf den abstrakten Mo- dellen verifizierten Eigenschaften durch die Verfeinerung erhalten werden. Insbesonde- re bei verteilten Systemen nimmt die Kommunikation der einzelnen Teilsysteme eine entscheidende Rolle für die Korrektheit des Gesamtverhaltens ein.
In dieser Arbeit wird eine Verfeinerungsdefinition für verteilte, adaptive Echtzeitsy- steme wie das an der Universität Paderborn entwickelte RailCab System vorgestellt, die eine korrekte Verfeinerung von Kommunikationsprotokollen in diesen Systemen be- schreibt. Die Definition basiert auf einem Timed Story Driven Modeling Ansatz, der einen für adaptive Systeme notwendigen gemeinsamen Formalismus für die Modellie- rung von Zustandsverhalten und Rekonfigurationen darstellt. Dabei wird das in Form von Realtime Statecharts vorliegende Zustandsverhalten auf um Zeit erweiterte Story Diagramme abgebildet.
Es werden verschiedene Ansätze für die Verifikation der korrekten Protokollverfei- nerung vorgestellt und bewertet. Durch die Integration des Algorithmus zur Verfeine- rungsverifikation mit den bestehenden Ansätzen der Mechatronic UML zur Verifikation von einfachen Komponenten und zur Verifikation von Koordinationsmustern wird nun die kompositionale Verifikation des Gesamtsystems vollständig ermöglicht.