In modern cloud architectures, multiple applications often run within the same clustered environment, sharing underlying resources. This resource sharing can cause interference among applications, leading to degraded latency and reduced system stability. As containerized microservices become increasingly central to cloud-native applications, their performance can suffer from complex interference scenarios related to resource competition. Meanwhile, most existing microservice approaches address interference either by detecting and localizing performance issues or by optimizing latency alone, without explaining why specific co-locations cause cross-application interference, and how this can inform service placement optimization. This work closes that gap by building a spatio-temporal data structure that captures the causal effects of cross-application interference. These causal effects are mathematically formalized as necessary and sufficient conditional probabilities that inform a multi-objective optimizer (Optuna). Cross-application profiling is used to simulate traces and estimate interference probabilities, while per-service latency baselines are provided by performance data, such as 95th-percentile response times (p95). Our approach supports network penalties, application isolation requirements, and adjustable weighting of necessary and sufficient causal metrics. Experimental results on real multi-application workloads show that interference-aware placements significantly reduce cross-application interference and improve response performance. Ultimately, the causality-driven multi-objective formulation gives cloud operators explicit control over interference, latency, and communication overhead when configuring service placements.

The growing size of graph-based modeling artifacts in model-driven engineering calls for techniques that enable efficient execution of graph queries. Incremental approaches based on the RETE algorithm provide an adequate solution in many scenarios, but are generally designed to search for query results over the entire graph. However, in certain situations, a user may only be interested in query results for a subgraph, for instance when a developer is working on a large model of which only a part is loaded into their workspace. In this case, the global execution semantics can result in significant computational overhead. To mitigate the outlined shortcoming, in this article we propose an extension of the RETE approach that enables local, yet fully incremental execution of graph queries, while still guaranteeing completeness of results with respect to the relevant subgraph. We empirically evaluate the presented approach via experiments inspired by a scenario from software development and with queries and data from an independent social network benchmark. The experimental results indicate that the proposed technique can significantly improve performance regarding memory consumption and execution time in favorable cases, but may incur a noticeable overhead in unfavorable cases.

Background] Efficient code review is essential in industrial software development, but writing high-quality Pull Request (PR) descriptions aligned with core software engineering competencies remains challenging. [Aims] To investigate Large Language Models (LLMs) as a reliable PR description assistant, we examined two research problems: (1) how developer competencies relate to real-world PR quality, and (2) how developers perceive PR quality and their variants (LLM-Improved). [Methods] We adopted six software engineering competencies to prompt six LLMs to score 212,687 PRs from 82 opensource projects spanning three repository archetypes. From these, we selected the top six PRs for a controlled experiment with 38 software professionals, using a$6 \times 6$Latin square design to measure preferences. The LLMs generated three variants of each original (O) PR: degraded (D), improved from the original (IO), and improved from the degraded (ID). We then compared these variants across LLMs for semantic, lexical, and stylistic similarity. [Results] Surprisingly, our controlled experiment with 38 software professionals showed that the ID variant was rated significantly higher than both the Original PR (O) and the LLMDegraded (D) one. However, the IO variant was not significantly better, and participants complained about their verbosity and the “AI tone”. Concerning generalizability, the six LLMs produced semantically similar PRs, but with high lexical and stylistic variation. [Conclusions] This suggests LLMs can enhance PR by providing missing structure but require guidance to retain human nuance. Overall, our findings support human-centered, modelaware integration of LLMs to strengthen competency-aligned code review.

Abstract The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results). To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.

Abstract Like conventional software projects, projects in model-driven software engineering require adequate management of multiple versions of development artifacts, importantly allowing living with temporary inconsistencies. In previous work, we have introduced multi-version models for model-driven software engineering, which allow checking well-formedness and finding merge conflicts for multiple versions of the same model at once. However, situations where different models are linked via automatic model transformations also have to be handled for multi-version models. In this paper, we propose a technique for jointly handling the transformation of multiple versions of a source model into corresponding versions of a target model. This enables the use of a more compact representation that may afford improved execution time of both the transformation and further analysis. Our approach is based on the well-known formalism of triple graph grammars and the aforementioned encoding of model version histories called multi-version models. In addition to batch transformation of an entire history, the technique covers incremental synchronization of changes in the framework of multi-version models. Our solution is complemented by a dedicated pattern matching technique for multi-version models. We show the correctness of our approach with respect to the standard semantics of triple graph grammars and conduct an empirical evaluation to investigate the performance of our technique regarding execution time and memory consumption. Our results indicate that the proposed solution affords lower memory consumption and may improve execution time for batch transformation of large version histories, but can also come with computational overhead in unfavorable cases.

Abstract In model-driven engineering, runtime monitoring of systems with complex dynamic structures is typically performed via a runtime model capturing a snapshot of the system state: the model is represented as a graph and properties of interest as graph queries which are evaluated over the model online. For temporal properties, history-aware runtime models encode a trace of timestamped snapshots, which is monitored via temporal graph queries. In this case, the query evaluation needs to consider that a trace may be incomplete, thus future changes to the model may affect current answers. So far there is no formal foundation for query-based monitoring over runtime models encoding incomplete traces. In this paper, we present a systematic and formal treatment of incomplete traces. First, we introduce a new definite semantics for a first-order temporal graph logic which only returns answers if no future change to the model will affect them. Then, we adjust the query evaluation semantics of a querying approach we previously presented, which is based on this logic, to the definite semantics of the logic. Lastly, we enable the approach to keep to its efficient query evaluation technique, while returning (the more costly) definite answers.

Abstract The correct operation of safety-critical cyber-physical systems is crucial. However, such systems often feature a large variability of start configurations, an intractably large state space, a high degree of uncertainty, or inherently unsafe behavior. A model of the expected system behavior starting in the current state can be used by look-ahead controllers to derive control decisions to avoid paths to safety violations when possible. However, the computational effort for deriving and analyzing the future system behavior is exponential in the look-ahead. In this paper, we employ Graph Transformation Systems (GTSs) for the modeling of expected system behavior. We then combine design-time and run-time control synthesis based on Supervisory Control Theory (SCT) achieving an exponential cost-reduction for a given controller look-ahead. For a fixed required reaction time of controllers, much longer look-aheads may therefore be employed. To illustrate and evaluate our approach, we consider a system where shuttles must avoid collisions with ambulances at level crossings.

The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on, e.g., concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces. We present an approach for the analysis of large-scale systems modeled as PTGTSs by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which shuttles drive on tracks of a large-scale topology and autonomously coordinate their local behavior with other shuttles nearby. For this running example, we verify that (a) shuttles can always make the expected forward progress using several properties, (b) shuttles never collide, and (c) shuttles are unlikely to execute emergency brakes in two scenarios. In our evaluation, we apply an implementation of our approach in the tool AutoGraph to our running example.

Abstract Modern software systems are intricate and operate in highly dynamic environments for which few assumptions can be made at design-time. This setting has sparked an interest in solutions that use a runtime model which reflects the system state and operational context to monitor and adapt the system in reaction to changes during its runtime. Few solutions focus on the evolution of the model over time, i.e., its history, although history is required for monitoring temporal behaviors and may enable more informed decision-making. One reason is that handling the history of a runtime model poses an important technical challenge, as it requires tracing a part of the model over multiple model snapshots in a timely manner. Additionally, the runtime setting calls for memory-efficient measures to store and check these snapshots. Following the common practice of representing a runtime model as a typed attributed graph, we introduce a language which supports the formulation of temporal graph queries, i.e., queries on the ordering and timing in which structural changes in the history of a runtime model occurred. We present a querying scheme for the execution of temporal graph queries over history-aware runtime models. Features such as temporal logic operators in queries, the incremental execution, the option to discard history that is no longer relevant to queries, and the in-memory storage of the model, distinguish our scheme from relevant solutions. By incorporating temporal operators, temporal graph queries can be used for runtime monitoring of temporal logic formulas. Building on this capability, we present an implementation of the scheme that is evaluated for runtime querying, monitoring, and adaptation scenarios from two application domains.

A dramatic transformation of our technical world towards smart cyber-physical systems can be currently observed. This transformation results in a networked technical world where besides the embedded systems with their interaction with the physical world the interconnection of these nodes in the cyber world becomes a key element. Furthermore, there is a strong trend towards smart systems where artificial intelligence techniques and in particular machine learning is employed to make software behave accordingly. This raises the question whether our capabilities to model these future embedded systems are ready to tackle the resulting challenges. In this presentation, we will first discuss how extensions of graph transformation systems can be employed to design and analyse the envisioned future cyber-physical systems with an emphasis on the synergies networking can offer and then characterise which challenges for the design, production, and operation of these systems and how they can be tacked with graph transformation systems. We will therefore discuss to what extent our current capabilities in particular concerning engineering with graph transformation systems match these challenges and where substantial improvements for the graph transformation systems have been crucial and will be crucial in the future. Models are used in classical engineering to plan systems upfront to maximise envisioned properties resp. minimise cost. For smart cyber-physical systems this decoupling of development-time and run-time considerations vanishes, and self-adaptation and runtime models have been advocated as concepts to shift some considerations to run-time. We will review the underlying causes for this shift to run-time, discuss some our work with graph transformation systems in this direction, and outline related open challenges and implications for future work for graph transformation systems to engineer smart cyber-physical systems.

Abstract The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on e.g. concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of probabilistic timed graph transformation systems is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces. We present an approach for the analysis of large-scale systems modeled as probabilistic timed graph transformation systems by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which we model shuttles driving on tracks of a large-scale topology and for which we verify that shuttles never collide and are unlikely to execute emergency brakes. In our evaluation, we apply an implementation of our approach to the running example.

Abstract Structural runtime models provide a snapshot of the constituents of a system and their state. Capturing the history of runtime models, i.e., previous snapshots, has been shown to be useful for a number of aims. Handling, however, history at runtime poses important challenges to tool support. We present the InTempo tool which is based on the Eclipse Modeling Framework and encodes runtime models as graphs. Key features of InTempo, such as, the integration of temporal requirements into graph queries, the in-memory storage of the model, and a systematic method to contain the model’s memory consumption, intend to address issues which seemingly place limitations on the available tool support. InTempo offers two operation modes which support both runtime and postmortem application scenarios.

Abstract Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the metric temporal graph logic (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool AutoGraph.

Runtime models provide a snapshot of a system at runtime at a desired level of abstraction. Via a causal connection to the modeled system and by employing model-driven engineering techniques, models support schemes for runtime adaptation where data from previous snapshots facilitates more informed decisions. Although runtime models and model-based adaptation techniques have been the focus of extensive research, schemes that treat the evolution of the model over time as a first-class citizen have only lately received attention. Consequently, there is a lack of sophisticated technology for such runtime models with history.

Self-adaptation can be realized in various ways. Rule-based approaches prescribe the adaptation to be executed if the system or environment satisfies certain conditions. They result in scalable solutions but often with merely satisfying adaptation decisions. In contrast, utility-driven approaches determine optimal decisions by using an often costly optimization, which typically does not scale for large problems. We propose a rule-based and utility-driven adaptation scheme that achieves the benefits of both directions such that the adaptation decisions are optimal, whereas the computation scales by avoiding an expensive optimization. We use this adaptation scheme for architecture-based self-healing of large software systems. For this purpose, we define the utility for large dynamic architectures of such systems based on patterns that define issues the self-healing must address. Moreover, we use pattern-based adaptation rules to resolve these issues. Using a pattern-based scheme to define the utility and adaptation rules allows us to compute the impact of each rule application on the overall utility and to realize an incremental and efficient utility-driven self-healing. In addition to formally analyzing the computational effort and optimality of the proposed scheme, we thoroughly demonstrate its scalability and optimality in terms of reward in comparative experiments with a static rule-based approach as a baseline and a utility-driven approach using a constraint solver. These experiments are based on different failure profiles derived from real-world failure logs. We also investigate the impact of different failure profile characteristics on the scalability and reward to evaluate the robustness of the different approaches.

Various kinds of typed attributed graphs can be used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformation can provide a formal model for defining state sequences. We consider the case where time may elapse between state changes and introduce a logic, called Metric Temporal Graph Logic (MTGL), to reason about such timed graph sequences. With this logic, we express properties on the structure and attributes of states as well as on the occurrence of states over time that are related by their inner structure, which no formal logic over graphs concisely accomplishes so far. Firstly, based on timed graph sequences as models for system evolution, we define MTGL by integrating the temporal operator until with time bounds into the well-established logic of (nested) graph conditions. Secondly, we outline how a finite timed graph sequence can be represented as a single graph containing all changes over time (called graph with history), how the satisfaction of MTGL conditions can be defined for such a graph and show that both representations satisfy the same MTGL conditions. Thirdly, we present how MTGL conditions can be reduced to (nested) graph conditions and show using this reduction that both underlying logics are equally expressive. Finally, we present an extension of the tool $$\textsc {AutoGraph}$$ allowing to check the satisfaction of MTGL conditions for timed graph sequences, by checking the satisfaction of the (nested) graph conditions, obtained using the proposed reduction, for the graph with history corresponding to the timed graph sequence.

An architectural runtime model is a causally connected abstract representation of a system that allows monitoring the system and adapting its configuration. Since systems are often constructed to operate continuously, the corresponding runtime model instances need to be long-living and available without interruptions. An interruption occurs if a model needs to be re-instantiated with a new version of the modeling language implementation to support other kinds of information. Adaptable runtime models instances can render such interruptions unnecessary and enable changing information demands at runtime. They support multiple abstraction levels for different model parts and allow adjusting over time which details of the system and its environment are represented. This helps to focus the attention for effective and efficient decision making. In this vision paper we present the fundamental idea of a generic modeling language for adaptable architectural runtime model instances and propose requirements and quality characteristics as criteria for its evaluation.

The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012 ) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp. simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata.

Summary Automated measurement programs are an efficient way of collecting, processing, and visualizing measures in large software development companies. The number of measurements in these programs is usually large, which is caused by a diversity of the needs of the stakeholders. In this paper, we present the application of the self‐healing concepts to assure the availability of measurements to the stakeholders without the need for effort‐intensive and costly manual interventions of the operators. We study the measurement infrastructure at one of the development units of a large infrastructure provider. In this paper, we present how the Monitor, Analyze, Plane, and Execute with Knowledge model was instantiated in a simplistic manner to reduce the need for manual intervention in the operation of the measurement systems. Based on the experiences from the 2 cases studied in this paper, we show how an evolution toward self‐healing measurement systems is done both with a dedicated failure taxonomy and with an effective straightforward handling of the most common errors in the execution. The mechanisms studied and presented in this paper show that self‐healing provides significant improvements to the operation of the measurement program and reduces the need for daily oversight by an operator for the measurement systems.

Good requirements engineering practices are essentialfor developing correct safety-critical systems. In this paper, we report our experience in combining existing rich modelinglanguages such as AADL (Architecture Analysis and DesignLanguage), URN (User Requirements Notation) and RDAL(Requirements Definition and Analysis Language) to supporta requirements engineering and design process as promotedby the FAA Requirements Engineering Management Handbook(REMH). Each of the combined language is well suited for thecapture of specific concerns of the REMH practices allowingreusing the capability from the individual languages but alsofrom their combined use. Our approach has been applied to thespecification and analysis of a medical device example from theREMH and shows several benefits due to the early discovery oferrors resulting from each modeling language and from theircombination. This experience also identifies important needs for automated model management not covered by current state-of the-art modeling techniques.

The development of self-adaptive software requires the engineering of an adaptation engine that controls the underlying adaptable software by feedback loops. The engine often describes the adaptation by runtime models representing the adaptable software and by activities such as analysis and planning that use these models. To systematically address the interplay between runtime models and adaptation activities, runtime megamodels have been proposed. A runtime megamodel is a specific model capturing runtime models and adaptation activities. In this article, we go one step further and present an executable modeling language for ExecUtable RuntimE MegAmodels (EUREMA) that eases the development of adaptation engines by following a model-driven engineering approach. We provide a domain-specific modeling language and a runtime interpreter for adaptation engines, in particular feedback loops. Megamodels are kept alive at runtime and by interpreting them, they are directly executed to run feedback loops. Additionally, they can be dynamically adjusted to adapt feedback loops. Thus, EUREMA supports development by making feedback loops explicit at a higher level of abstraction and it enables solutions where multiple feedback loops interact or operate on top of each other and self-adaptation co-exists with offline adaptation for evolution.

Teaching Requirements Engineering needs to be a realistic experience. Otherwise the students might not understand the repercussions of failing to gather requirements correctly. While simulated stakeholders are always a feasible option, only real stakeholders offer an authentic experience since only they are impacted by the system that is being specified. In this paper, we present our experiences of cooperating with the non-governmental organization (NGO) Wasserwacht. In a first requirements engineering course, nine graduate students elicited requirements by interviewing a dozen heterogeneous stakeholders. In a subsequent bachelor's project, four undergraduate students continued by implementing the software system based on these requirements. We discuss the authenticity of our requirements engineering setting, the influence of the collected requirements on the follow-up implementation project and how the Wasserwacht benefited from this cooperation.

The proper composition of independently developed components of an embedded real-time system is complicated due to the fact that besides the functional behavior also the non-functional properties and in particular the timing have to be compatible. A number of formal approaches have been developed, which try to guide the upfront decomposition of the embedded real-time system into components such that integration problems related to timing can be excluded. However, the proposed solutions come with severe limitations or require an analysis that does not scale such that these approaches are hardly applicable in practice. In this paper, we present an approach that ensures real-time compatibility by modeling the component behavior with timed automata and by only locally checking that the component is compatible concerning timing. The effort to establish the required guarantees for the integration scales as only local checks are employed. An AUTOSAR application example from the automotive domain is employed to demonstrate the applicability and scalability of the approach.

One of the multiple technical factors which affect changeability of software is model-driven engineering (MDE), where often several models and a multitude of manual as well as automated development activities have to be mastered to derive the final software product. The ability to change software with only reasonable costs, however, is of uppermost importance for the iterative and incremental development of software as well as agile development in general. Thus, the effective applicability of agile processes is influenced by the used MDE activities. However, there is currently no approach available to systematically detect and handle such risks to the changeability that result from the embedded MDE activities. In this paper we extend our beforehand-introduced process modeling approach by a notion of process pattern to capture typical situations that can be associated with risk or benefit with respect changeability. In addition, four candidates for the envisioned process patterns are presented in detail in the paper. Further, we developed strategies to handle changeability risks associated to these process patterns.

Model-Driven Engineering (MDE) mixes up manual activities, like coding or modeling, with automated activities, such as transformation or generation steps, which can lead to constraints on the development process. Currently, we know little about such constraints. For gaining more knowledge about this it is necessary to capture and compare MDE activities from practice to identify reoccurring structures that can be associated to constraints on the software development process. However, current techniques to capture MDE activities are not sufficient for comparison. Therefore, we developed a new approach to characterize activities based on relations between consumed and produced artifacts. Further, we evaluated this approach by applying it to activities from industrial case studies. Thereby, we found that our approach is applicable to capture complex industrial activities and that the identification of reoccurring structures is possible. These results enable future research about the influence of MDE activities on software development processes.

The Software Engineering for Adaptive and Self-managing Systems (SEAMS) workshop has consolidated the interest in the software engineering community on self-adaptive and self-managing systems. SEAMS provides a forum for researchers and practitioners to share new results, discuss challenging issues, raise awareness, and promote collaboration within the community. The SEAMS 2010 workshop aims to continue the success of previous ICSE SEAMS workshops: in Shanghai in 2006, in Minneapolis in 2007, in Leipzig in 2008, and in Vancouver in 2009.

The next generation of advanced mechatronic systems is expected to enhance their functionality and improve their performance by context-dependent behavior. Therefore, these systems require to represent information about the complex environment and changing sets of collaboration partners internally. This requirement is in contrast to the usually assumed static structures for embedded systems. In this paper, we present a model-driven approach which overcomes this situation by supporting dynamic data structures while still guaranteeing that valid worst-case execution times can be derived. It supports a flexible resource management which avoids to operate with the prohibitive coarse worst-case boundaries but instead supports to run applications in different profiles which guarantee different resource requirements and put unused resources in a profile at other applications' disposal. By supporting the proper estimation of worst case execution time (WCET) and worst case number of iteration (WCNI) at runtime, we can further support to create new profiles, add or remove them at runtime in order to minimize the over-approximation of the resource consumption resulting from the dynamic data structures required for the outlined class of advanced systems.

In this tool demonstration we present an implementation for interactively validating requirements for multi-user software systems and the processes they support with end users. The tool combines the advantages of requirements animation and scenario synthesis to gather stakeholder feedback and create a common understanding amongst stakeholders. Additionally, the users' behavior during the simulation is captured and used to automatically derive new behavioral specifications.

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.

The performance of autonomous vehicles could be drastically improved if ad-hoc networking and suitable real-time coordination is employed to optimize and improve the joint behavior of multiple autonomous units. However, due to ad-hoc connections and the real-time interaction the correctness and safety of such coordinated autonomous units is very hard to ensure. In this paper we present how service- oriented real-time coordination can be employed to achieve this goal. Based on the proper real-time coordination between two or more vehicles captured by a service contract, we focus on structural changes and the instantiation and termination of service contracts which is a crucial prerequisite for a safe system operation. We present how the structural changes and the service contract creation/deletion can be modeled by a well-defined UML subset consisting of class and object diagrams with collaborations as well as well-defined behavioral rules can be verified taking the dynamic structural changes due to the ad-hoc networking as well as the real-time coordination into account. The new verification technique is outlined and the application of the technique for an application example is presented.

The next generation of advanced mechatronic systems is expected to use its software to exploit local and global networking capabilities to enhance their functionality and to adapt their local behavior when beneficial. Such systems will therefore include complex hard real-time coordination at the network level. This coordination is further reflected locally by complex reconfiguration in form of mode management and control algorithms. We present in this paper the integration of two tools which allow the integrated specification of real-time coordination and traditional control engineering specifically targeting the required complex reconfiguration of the local behavior.

The next generation of networked mechatronic systems will be characterized by complex coordination and structural adaptation at run-time. Crucial safety properties have to be guaranteed for all potential structural configurations. Testing cannot provide safety guarantees, while current model checking and theorem proving techniques do not scale for such systems. We present a verification technique for arbitrarily large multi-agent systems from the mechatronic domain, featuring complex coordination and structural adaptation. We overcome the limitations of existing techniques by exploiting the local character of structural safety properties. The system state is modeled as a graph, system transitions are modeled as rule applications in a graph transformation system, and safety properties of the system are encoded as inductive invariants (permitting the verification of infinite state systems). We developed a symbolic verification procedure that allows us to perform the computation on an efficient BDD-based graph manipulation engine, and we report performance results for several examples.

Software is becoming present in every aspect of our lives, pushing us inevitably towards a world of ambient computing systems. Multi-agent systems (MAS) are a prominent technology which facilitates modeling and development of large-scale distributed systems. In recent years, software engineering research has focused on methodologies and techniques for improving MAS design and implementation. However, making large MAS dependable is still an open issue. The Fifth Workshop on Software Engineering for Large-Scale Multi-Agent Systems (SELMAS 2006) aims to bring together academic, industrial and commercial communities interested in agent-oriented software engineering topics to discuss the different technologies being defined and used in the development of dependable MAS.

In advanced mechatronic systems, software was traditionally employed late in the development process for cost-effectively realizing the required control functionality. Today however, software has become one of the main drivers for innovation, enabling cost-effective variants and online reconfiguration. During the development of mechatronic systems, different alternative principle solutions are usually systematically evaluated w.r.t. physical and economic requirements and constraints. We refine this step by performing a differentiated analysis factoring in relevant environmental influences. For multiple variants of a product line, the evaluation results can easily be reused by adjusting the weights of individual requirements and the relevance of different environmental situations. Taking synergies during development and production into account, a set of alternatives can then be identified which provides high performance at a low cost for the product line. Based on the refined analysis, we can furthermore identify combinations of alternative solutions that offer a more complete coverage of the required operation conditions or a more cost-effective solution by performing an online software reconfiguration in response to changes in the environment

No abstract available

Today, complex, networked, self-adaptive mechatronic systems which integrate advanced control engineering and software engineering concepts within a single software system are envisioned. These systems adapt their structures at runtime to react to detected environmental changes, to change their system goals, or to react to a change of the system structure. To enable the development of such systems, an integration of object-oriented modeling techniques such as UML and control theory approaches such as functional block modeling is required. Thereby, the successful visual modeling concepts of control engineering should be preserved, as otherwise wide acceptance in industry, which is mainly dominated by control engineers, is very unlikely. In this paper, we present such a visual integration for UML 2.0 components, statecharts, and block diagrams developed within the MECHATRONlC UML approach. It permits to graphically model reconfiguration between several pre-defined configurations with statecharts and instance diagrams as well as to specify the flexible assembly of control configuration if needed by means of visual reconfiguration rules.

Summary form only given. Visual modeling techniques play an important role in the design and understanding of complex, software intensive systems. Block diagrams in systems engineering and the Unified Modeling Language (UML) in software engineering, are prominent examples of such visual modeling techniques.

Mechatronic systems are embedded software systems with hard real-time requirements. Predictability is of paramount importance for these systems. Thus, their design has to take the worst-case into account and the maximal required resources are usually allocated upfront by each process. This is safe, but usually results in a rather poor resource utilization. If in contrast resource-aware agents, which are able to allocate and free resources in a controllable safe manner, instead of thumb processes are present, then a resource manager will coordinate their safe dynamic resource allocation at run time. But given such a resource manager, how can we transform thumb processes into smart resource-aware agents? Starting with mechatronic components that describe their reconfiguration by means of statecharts, we present how to automatically synthesize the additional information and code, which enables a process to become a resource-aware agent.

The development of complex mechatronic systems requires a careful and ideally verifiable design. In addition, engineers from different disciplines, namely mechanical, electrical and software engineering, have to cooperate. The current technology is to use block diagrams including discrete blocks with statecharts for the design and verification of such systems. This does not adequately support the verification of large systems which improve the system behavior at run-time by means of online reconfiguration of its controllers because the system as whole has to be verified. It also does not support cooperative interdisciplinary work because a white-box view on all blocks involved in the online reconfiguration is required. This paper proposes a rigorous component concept based on the notion of UML component diagrams which enables modular composition and decomposition of complex systems with online reconfiguration given by hierarchical hybrid component specifications. The approach enables compatibility checks between components that are often independently developed (across the different disciplines) and supports compositional model checking based on a rigorously defined semantics.

Current techniques for the verification of software as e.g. model checking are limited when it comes to the verification of complex distributed embedded real-time systems. Our approach addresses this problem and in particular the state explosion problem for the software controlling mechatronic systems, as we provide a domain specific formal semantic definition for a subset of the UML 2.0 component model and an integrated sequence of design steps. These steps prescribe how to compose complex software systems from domain-specific patterns which model a particular part of the system behavior in a well-defined context. The correctness of these patterns can be verified individually because they have only simple communication behavior and have only a fixed number of participating roles. The composition of these patterns to describe the complete component behavior and the overall system behavior is prescribed by a rigorous syntactic definition which guarantees that the verification of component and system behavior can exploit the results of the verification of individual patterns.

How do you organize an "industrial strength" one semester educational programming project for up to 200 second year students? This paper reports on four years of experience with such projects at the University of Paderborn and the University of Braunschweig. Key properties of our project design are: starting with an existing large application, regular hard deadlines with peer reviews and presentations to a large audience, working in groups, applying project and configuration management tools, a standard system architecture with interchangeable components and competing software agents, quality assurance and standard conformance testing through final overall system integration spanning all groups, and exposure to real-world project threats.

The specification of intra- and inter-organizational workflows in a manner which scales up to complex workflows across division and company borders is a central issue for present-day workflow modeling. The approach described integrates standard object oriented structure modeling using UML diagrams with Petri net techniques for specifying behavior in order to provide an adequate support for modeling all aspects of workflows. The approach puts its emphasis on structuring and abstraction techniques to manage the size and complexity of real life applications. A contract mechanism is used to ensure the independence of different companies and to permit the reuse of partial workflows in a manner which is secure for the offering as well as the usage side.