Jan Oliver Ringert

Dhaminda B. Abeywickrama, Amel Bennaceur, Greg Chance et al.

As autonomous systems (AS) increasingly become part of our daily lives, ensuring their trustworthiness is crucial. In order to demonstrate the trustworthiness of an AS, we first need to specify what is required for an AS to be considered trustworthy. This roadmap paper identifies key challenges for specifying for trustworthiness in AS, as identified during the "Specifying for Trustworthiness" workshop held as part of the UK Research and Innovation (UKRI) Trustworthy Autonomous Systems (TAS) programme. We look across a range of AS domains with consideration of the resilience, trust, functionality, verifiability, security, and governance and regulation of AS and identify some of the key specification challenges in these domains. We then highlight the intellectual challenges that are involved with specifying for trustworthiness in AS that cut across domains and are exacerbated by the inherent uncertainty involved with the environments in which AS need to operate.

Mohamed Parvez Aslam, Bojan Derajic, Mohamed-Khalil Bouzidi et al.

Safe navigation in pedestrian-rich environments remains a key challenge for autonomous robots. This work evaluates the integration of a deep learning-based Social-Implicit (SI) pedestrian trajectory predictor within a Model Predictive Control (MPC) framework on the physical Continental Corriere robot. Tested across varied pedestrian densities, the SI-MPC system is compared to a traditional Constant Velocity (CV) model in both open-loop prediction and closed-loop navigation. Results show that SI improves trajectory prediction - reducing errors by up to 76% in low-density settings - and enhances safety and motion smoothness in crowded scenes. Moreover, real-world deployment reveals discrepancies between open-loop metrics and closed-loop performance, as the SI model yields broader, more cautious predictions. These findings emphasize the importance of system-level evaluation and highlight the SI-MPC framework's promise for safer, more adaptive navigation in dynamic, human-populated environments.

Shahar Maoz, Jan Oliver Ringert

Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications. We present the language and give an overview of the tool set.

Shahar Maoz, Jan Oliver Ringert

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face when using GR(1) synthesis for the development of a reactive robotic system. In the case study we developed two variants of a forklift controller, deployed on a Lego robot. The case study employs LTL specification patterns as an extension of the GR(1) specification language, an examination of two specification variants for execution scheduling, traceability from the synthesized controller to constraints in the specification, and generated counter strategies to support understanding reasons for unrealizability. We present the specifications we developed, our observations, and challenges faced during the case study.

Bernhard Rumpe, Christoph Schulze, Michael von Wenckstern et al.

Embedded software systems, e.g. automotive, robotic or automation systems are highly configurable and consist of many software components being available in different variants and versions. To identify the degree of reusability between these different occurrences of a component, it is necessary to determine the functional backward and forward compatibility between them. Based on this information it is possible to identify in which system context a component can be replaced safely by another version, e.g. exchanging an older component, or variant, e.g. introducing new features, to achieve the same functionality. This paper presents a model checking approach to determine behavioral compatibility of Simulink models, obtained from different component variants or during evolution. A prototype for automated compatibility checking demonstrates its feasibility. In addition implemented optimizations make the analysis more efficient, when the compared variants or versions are structurally similar. A case study on a driver assistance system provided by Daimler AG shows the effectiveness of the approach to automatically compare Simulink components.

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

This book presents MontiArcAutomaton, a modeling language for architecture and be- havior modeling of Cyber-Physical Systems as interactive Component & Connector mod- els. MontiArcAutomaton extends the Architecture Description Language MontiArc with automata to describe component behavior. The modeling language MontiArcAutomaton provides syntactical elements for defin- ing automata with states, variables, and transitions inside MontiArc components. These syntactical elements and a basic set of well-formedness rules provide the syntax for a fam- ily of modeling languages for state-based behavior modeling in Component & Connector architectures. We present two concrete language profiles with additional well-formedness rules to model time-synchronous component behavior and untimed, event-driven behav- ior of components. This book gives an overview of the MontiArcAutomaton language including examples, a language reference, and a context-free grammar for MontiArcAutomaton models. It also provides syntax definition, well-formedness rules, and semantics for two language profiles. We summarize projects and case studies applying MontiArcAutomaton. MontiArcAutomaton is implemented using the DSL framework MontiCore. Available tools include a textual editor with syntax highlighting and code completion as well as a graphical editor and a powerful and extensible code generation framework for target languages including EMF, Java, Mona, and Python.

Jan Oliver Ringert, Alexander Roth, Bernhard Rumpe et al.

Engineering software for robotics applications requires multidomain and application-specific solutions. Model-driven engineering and modeling language integration provide means for developing specialized, yet reusable models of robotics software architectures. Code generators transform these platform independent models into executable code specific to robotic platforms. Generative software engineering for multidomain applications requires not only the integration of modeling languages but also the integration of validation mechanisms and code generators. In this paper we sketch a conceptual model for code generator composition and show an instantiation of this model in the MontiArc- Automaton framework. MontiArcAutomaton allows modeling software architectures as component and connector models with different component behavior modeling languages. Effective means for code generator integration are a necessity for the post hoc integration of applicationspecific languages in model-based robotics software engineering.

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

Component-based software engineering aims to reduce software development effort by reusing established components as building blocks of complex systems. Defining components in general-purpose programming languages restricts their reuse to platforms supporting these languages and complicates component composition with implementation details. The vision of model-driven engineering is to reduce the gap between developer intention and implementation details by lifting abstract models to primary development artifacts and systematically transforming these into executable systems. For sufficiently complex systems the transformation from abstract models to platform-specific implementations requires augmentation with platform-specific components. We propose a model-driven mechanism to transform platform-independent logical component & connector architectures into platform-specific implementations combining model and code libraries. This mechanism allows to postpone commitment to a specific platform and thus increases reuse of software architectures and components.

Hans Grönninger, Jan Oliver Ringert, Bernhard Rumpe

In this paper, we present an approach to define the semantics for object-oriented modeling languages. One important property of this semantics is to support underspecified and incomplete models. To this end, semantics is given as predicates over elements of the semantic domain. This domain is called the system model which is a general declarative characterization of object systems. The system model is very detailed since it captures various relevant structural, behavioral, and interaction aspects. This allows us to re-use the system model as a domain for various kinds of object-oriented modeling languages. As a major consequence the integration of language semantics is straight-forward. The whole approach is supported by tools that do not constrain the semantics definition's expressiveness and flexibility while making it machinecheckable.

Arne Haber, Jan Oliver Ringert, Bernhard Rumpe

This report presents MontiArc, a modeling language for the description of Component & Connector architectures. A component is a unit executing computations and/or storing data. Information flow between components is modeled via unidirectional connectors connecting typed, directed ports of the interfaces of components. Language features of the ADL MontiArc include hierarchical decomposition of components, subtyping by structural inheritance, component type definitions and reference declarations for reuse, generic component types and configurable components, syntactic sugar for connectors, and controlled implicit creation of connections and subcomponent declarations. This technical report gives an overview of the MontiArc language and is a reference for the MontiArc grammar intended to enable reuse and extension of MontiArc and MontiArc related tools. MontiArc is implemented using the DSL framework MontiCore. Available tools include an editor with syntax highlighting and code completion as well as a simulation framework with a Java code generator.

Markus Look, Antonio Navarro Perez, Jan Oliver Ringert et al.

Robots belong to a class of Cyber-Physical Systems where complex software as a mobile device has to full tasks in a complex environment. Modeling robotics applications for analysis and code generation requires modeling languages for the logical software architecture and the system behavior. The MontiArcAutomaton modeling framework integrates six independently developed modeling languages to model robotics applications: a component & connector architecture description language, automata, I/O tables, class diagrams, OCL, and a Java DSL. We describe how we integrated these languages into MontiArcAutomaton a-posteriori in a black-box integration fashion.

Arne Haber, Jan Oliver Ringert, Bernhard Rumpe

Integrating architectural elements with a modern programming language is essential to ensure a smooth combination of architectural design and programming. In this position statement, we motivate a combination of architectural description for distributed, asynchronously communicating systems and Java as an example for such an integration. The result is an ordinary programming language, that exhibits architecture, data structure and behavior within one view. Mappings or tracing between different views is unnecessary. A prototypical implementation of a compiler demonstrates the possibilities and challenges of architectural programming.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Models are heavily used in software engineering and together with their systems they evolve over time. Thus, managing their changes is an important challenge for system maintainability. Existing approaches to model differencing concentrate on heuristics matching between model elements and on finding and presenting differences at a concrete or abstract syntactic level. While showing some success, these approaches are inherently limited to comparing syntactic structures. This paper is a manifesto for research on semantic model differencing. We present our vision to develop semantic diff operators for model comparisons: operators whose input consists of two models and whose output is a set of diff witnesses, instances of one model that are not instances of the other. In particular, if the models are syntactically different but there are no diff witnesses, the models are semantically equivalent. We demonstrate our vision using two concrete diff operators, for class diagrams and for activity diagrams. We motivate the use of semantic diff operators, brie y discuss the algorithms to compute them, list related challenges, and show their application and potential use as new fundamental building blocks for change management in model-driven engineering.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from an AD represents an executed action of this AD with interleaved execution of concurrent branches. An implementation of the given translation was used in the context of semantic differencing for ADs [MRR11]. We define the translation and give two examples, showing ADs and their complete representation in SMV.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Class diagrams (CDs), which specify classes and the relationships between them, are widely used for modeling the structure of object-oriented systems. As models, programs, and systems evolve over time, during the development lifecycle and beyond it, effective change management is a major challenge in software development, which has attracted much research efforts in recent years. In this paper we present cddiff, a semantic diff operator for CDs. Unlike most existing approaches to model comparison, which compare the concrete or the abstract syntax of two given diagrams and output a list of syntactical changes or edit operations, cddiff considers the semantics of the diagrams at hand and outputs a set of diff witnesses, each of which is an object model that is possible in the first CD and is not possible in the second. We motivate the use of cddiff, formally define it, and show how it is computed. The computation is based on a reduction to Alloy. The work is implemented in a prototype Eclipse plug-in. Examples show the unique contribution of our approach to the state-of-the-art in version comparison and evolution analysis.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce modal object diagrams (MODs), which extend the classical OD language with positive/negative and example/invariant modalities. The extended language allows the designer to specify not only positive example models but also negative examples, ones that the system should not allow, positive invariants, ones that all system's snapshots should include, and negative invariants, ones that no system snapshot is allowed to include. Moreover, as a primary application of the extended language we provide a formal verification technique that decides whether a given class diagram satisfies (i.e., models) a multi-modal object diagrams specification. In case of a negative answer, the technique outputs relevant counterexample object models, as applicable. The verification is based on a reduction to Alloy. The ideas are implemented in a prototype Eclipse plug-in. Examples show the usefulness of the extended language in specifying structural requirements of object-oriented systems in an intuitive yet expressive way.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Activity diagrams (ADs) have recently become widely used in the modeling of workflows, business processes, and web-services, where they serve various purposes, from documentation, requirement definitions, and test case specifications, to simulation and code generation. As models, programs, and systems evolve over time, understanding changes and their impact is an important challenge, which has attracted much research efforts in recent years. In this paper we present addiff, a semantic differencing operator for ADs. Unlike most existing approaches to model comparison, which compare the concrete or the abstract syntax of two given diagrams and output a list of syntactical changes or edit operations, addiff considers the Semantics of the diagrams at hand and outputs a set of diff witnesses, each of which is an execution trace that is possible in the first AD and is not possible in the second. We motivate the use of addiff, formally define it, and show two algorithms to compute it, a concrete forward-search algorithm and a symbolic xpoint algorithm, implemented using BDDs and integrated into the Eclipse IDE. Empirical results and examples demonstrate the feasibility and unique contribution of addiff to the state-of-the-art in version comparison and evolution analysis.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

We present CD2Alloy, a novel, powerful translation of UML class diagrams (CDs) to Alloy. Unlike existing translations, which are based on a shallow embedding strategy, and are thus limited to checking consistency and generating conforming object models of a single CD, and support a limited set of CD language features, CD2Alloy uses a deeper embedding strategy. Rather than mapping each CD construct to a semantically equivalent Alloy construct, CD2Alloy defines (some) CD constructs as new concepts within Alloy. This enables solving several analysis problems that involve more than one CD and could not be solved by earlier works, and supporting an extended list of CD language features. The ideas are implemented in a prototype Eclipse plug-in. The work advances the state-of-the-art in CD analysis, and can also be viewed as an interesting case study for the different possible translations of one modeling language to another, their strengths and weaknesses.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Checking consistency between an object diagram (OD) and a class diagram (CD) is an important analysis problem. However, several variations in the semantics of CDs and ODs, as used in different contexts and for different purposes, create a challenge for analysis tools. To address this challenge in this paper we investigate semantically configurable model analysis. We formalize the variability in the languages semantics using a feature model: each configuration that the model permits induces a different semantics. Moreover, we develop a parametrized analysis that can be instantiated to comply with every legal configuration of the feature model. Thus, the analysis is semantically congured and its results change according to the semantics induced by the selected feature configuration. The ideas are implemented using a parametrized transformation to Alloy. The work can be viewed as a case study example for a formal and automated approach to handling semantic variability in modeling languages.

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

Robotics poses a challenge for software engineering as the vast numbers of different robot platforms impose different requirements on robot control architectures. The platform dependent development of robotic applications impedes reusability and portability. The lack of reusability hampers broad propagation of robotics applications. The MontiArcAutomaton architecture and behavior modeling framework provides an integrated, platform independent structure and behavior modeling language with an extensible code generation framework. MontiArcAutomaton's central concept is encapsulation and decomposition known from Component & Connector Architecture Description Languages. This concept is extended from the modeling language to the code generation and target runtime framework to bridge the gap of platform specific and independent implementations along well designed interfaces. This facilitates the reuse of robot applications and makes their development more efficient.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

Fundamental building blocks for managing and understanding software evolution in the context of model-driven engineering are differencing operators one can use for model comparisons. Semantic model differencing deals with the definition and computation of semantic diff operators for model comparison, operators whose input consists of two models and whose output is a set of diff witnesses, instances of one model that are not instances of the other. However, in many cases the complete set of diff witnesses is too large to be efficiently computed and effectively presented. Moreover, many of the witnesses are very similar and hence not interesting. Thus, an important challenge of semantic differencing relates to witness selection and presentation. In this paper we propose to address this challenge using a summarization technique, based on a notion of equivalence that partitions the set of diff witnesses. The result of the computation is a summary set, consisting of a single representative witness from each equivalence class. We demonstrate our ideas using two concrete diff operators, for class diagrams and for activity diagrams, where the computation of the summary set is efficient and does not require the enumeration of all witnesses.

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

Software development for robotics applications is a sophisticated endeavor as robots are inherently complex. Explicit modeling of the architecture and behavior of robotics application yields many advantages to cope with this complexity by identifying and separating logically and physically independent components and by hierarchically structuring the system under development. On top of component and connector models we propose modeling the requirements on the behavior of robotics software components using I/O! automata. This approach facilitates early simulation of requirements model, allows to subject these to formal analysis and to generate the software from them. In this paper, we introduce an extension of the architecture description language MontiArc to model the requirements on components with I/O!automata, which are defined in the spirit of Martin Glinz Statecharts for requirements modeling [10]. We furthermore present a case study based on a robotics application generated for the Lego NXT robotic platform.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

This position paper provides an interim summary on the goals and current state of our ongoing research project on semantic model differencing for software evolution. We describe the basics of semantic model differencing, give two examples from our recent work, and discuss future challenges in taking full advantage of the potential of semantic differencing techniques in the context of models' evolution.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

We present component and connector (C&C) views, which specify structural properties of component and connector models in an expressive and intuitive way. C&C views provide means to abstract away direct hierarchy, direct connectivity, port names and types, and thus can crosscut the traditional boundaries of the implementation-oriented hierarchical decomposition of systems and sub-systems, and reflect the partial knowledge available to different stakeholders involved in a system's design. As a primary application for C&C views we investigate the synthesis problem: given a C&C views specification, consisting of mandatory, alternative, and negative views, construct a concrete satisfying C&C model, if one exists. We show that the problem is NP-hard and solve it, in a bounded scope, using a reduction to SAT, via Alloy. We further extend the basic problem with support for library components, specification patterns, and architectural styles. The result of synthesis can be used for further exploration, simulation, and refinement of the C&C model or, as the complete, final model itself, for direct code generation. A prototype tool and an evaluation over four example systems with multiple specifications show promising results and suggest interesting future research directions towards a comprehensive development environment for the structure of component and connector designs.

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

Software development for service robotics is inherently complex. Even a single robot requires the composition of several sensors, actuators, and software modules. The systems are usually developed by groups of domain experts, rarely software engineering experts. Thus the resulting software systems are monolithic programs solving a single problem on a single platform. We claim modeling of both structure and behavior of robots in a modular way leads to better reusable software. We report on a study about the modeling of robotics software with the structure and behavior modeling language MontiArcAutomaton. This study assesses the benefits and difficulties of model-based robotics software development using MontiArc-Automaton. Our findings are based on a survey, discussions with the participants, and key figures from their development behavior. We present the project, our study, lessons learned, and future work based on the insights gained

Jan Oliver Ringert, Bernhard Rumpe, Andreas Wortmann

Software development for Cyber-Physical Systems (CPS) is a sophisticated activity as these systems are inherently complex. The engineering of CPS requires composition and interaction of diverse distributed software modules. Describing both, a systems architecture and behavior in integrated models, yields many advantages to cope with this complexity: the models are platform independent, can be decomposed to be developed independently by experts of the respective fields, are highly reusable and may be subjected to formal analysis. In this paper, we introduce a code generation framework for the MontiArcAutomaton modeling language. CPS are modeled as Component & Connector architectures with embedded I/O! automata. During development, these models can be analyzed using formal methods, graphically edited, and deployed to various platforms. For this, we present four code generators based on the MontiCore code generation framework, that implement the transformation from MontiArcAutomaton models to Mona (formal analysis), EMF Ecore (graphical editing), and Java and Python (deployment. Based on these prototypes, we discuss their commonalities and differences as well as language and application specific challenges focusing on code generator development.

Shahar Maoz, Jan Oliver Ringert, Bernhard Rumpe

The structure of component and connector (C&C) models, which are used in many application domains of software engineering, consists of components at different containment levels, their typed input and output ports, and the connectors between them. C&C views, presented in [24], can be used to specify structural properties of C&C models in an expressive and intuitive way. In this work we address the verification of a C&C model against a C&C view and present efficient (polynomial) algorithms to decide satisfaction. A unique feature of our work, not present in existing approaches to checking structural properties of C&C models, is the generation of witnesses for satisfaction/non-satisfaction and of short naturallanguage texts, which serve to explain and formally justify the verification results and point the engineer to its causes. A prototype tool and an evaluation over four example systems with multiple views, performance and scalability experiments, as well as a user study of the usefulness of the witnesses for engineers, demonstrate the contribution of our work to the state-of-the-art in component and connector modeling and analysis.