Increasing automation is an ongoing effort across various mobility sectors, including the railway domain, promising to address issues such as sustainability, lack of personnel, and enhancing mobility in rural areas. The development of automated railway systems is a challenging task and the validation of safety of such systems in open context remains an open topic. Simulation-based validation of driverless trains can help to ensure safe operation. This paper presents an extension of the open-source train simulator OpenRails to enable doing a closed-loop simulation with the goal of validating the behavior of a system under test within a simulated environment. We propose a possible scenario-based validation approach and present the whole loop including description of an abstract scenario using Traffic Sequence Charts, derivation of a concrete instance of this abstract scenario, and a novel closed-loop play-out. We share our experiences and the current state of our work and give outlook on future directions.

Transitioning automated driving systems to complex operational domains disproportionally increases demands on verification activities . In the worst case, the operational domain can not be covered by a manageable set of logical scenarios. An anticipated solution is to use abstract scenarios, which increase coverage while still enabling formal methods. However, established verification approaches must be adapted for abstract scenarios. In this work, we consider the generation of simulatable test suites from abstract scenarios. For this, we use Traffic Sequence Charts (TSCs), a visual yet formal scenario description language based on first order logic. We propose an SMT-based process for generating concrete test cases that can be simulated in e.g. CARLA. This theoretical framework is compiled into an architecture and a prototypical implementation called TSC2CARLA. An evaluation on a set of non-trivial examples yields initial evidence for the feasibility of our approach.

Abstract In the automotive domain, scenario-based development is the answer to the increasing complexity of highly automated driving functions. Scenario-based methods cluster the large scenario space by so-called abstract scenarios which can be used to sample an infinite number of concrete scenarios. Because abstract scenarios constrain driving maneuvers by excessive use of additional constraints, constraint solving techniques may be required to find concrete scenario instances. In order to guarantee correctness of simulation runs with respect to the abstract scenario, realistic vehicle dynamics need to be considered during the instantiation process. This work proposes an encoding scheme for abstract scenarios into linear constraint systems for the generation of correct-by-construction concrete scenarios. It covers both temporal and spatial aspects of the abstract scenario, as well as simple, but realistic vehicle dynamics. The applicability of the method is shown by demonstrating it on a set of basic driving maneuvers. This paper extends the previous version by presenting further experimental results and giving an overview over practical applications.

The MobSTr dataset contains a number of artifacts for an autonomous driver assistance system, ranging from textual requirements to models for system design and models relevant to safety assurance. The artifacts provided are connected with traceability links created and managed with Eclipse Capra, an open source traceability management tool. The dataset builds upon a custom traceability information model that provides type safety and semantics for the trace links. MobSTr is intended for researchers that work on software and systems traceability as well as on model-based safety assurance. It is already being used in a number of studies, including research on trace link consistency, change impact analysis, and automated analysis of safety and timing requirements.

Traceability management relies on a supporting model, the traceability information model (TIM), that defines which types of relationships exist between which artifacts and contains additional constraints such as multiplicities. Constructing a TIM that is fit for purpose is crucial to ensure that a traceability strategy yields the desired benefits. However, which design decisions are critical in the construction of TIMs and which impact they have on the usefulness and applicability of traceability is still an open question. In this paper, we use two cases of TIMs constructed for safety-critical, automotive systems with industrial safety experts, to identify key design decisions. We also propose a comparison scheme for TIMs based on a systematic literature review and evaluate the two cases as well as TIMs from the literature according to the scheme. Based on our analyses, we thus derive key insights into TIM construction and the design decisions that ensure that a TIM is fit for purpose.

Domain-specific modeling languages (DSMLs) are usually defined by meta-modeling using the Object Constraint Language (OCL) for specifying invariants. This approach is purely declarative in the sense that instance construction is not supported. In contrast, grammar-based language definition incorporates the stepwise construction of instances by applying production rules. Since the underlying structure of models are generally graphs, graph grammars are well suited to define modeling languages. Establishing a formal relation between meta-modeling and graph grammars opens up the possibility to integrate techniques of both fields. This integration can be advantageously used for optimizing DSML definition. We follow an approach where a meta-model is translated to a type graph with a set of nested graph constraints. While previous meta-model translations neglected OCL constraints, we focus on the translation of Essential OCL invariants to nested graph constraints in this paper. We show that a model satisfies an Essential OCL invariant iff its corresponding instance graph satisfies the corresponding nested graph constraint. In addition, nested graph constraints can be translated to application conditions of graph transformation rules. Composing both translations, an instance-generating graph grammar can be equipped with application conditions such that it generates instances of the original meta-model only.

We present new findings for a new class of fault-tolerant distributed algorithms based on a concept called region adherence. A region-adherent algorithm upper-bounds the violation of safety due to faults in space. Region adherence counter-poses the concept of self-stabilization which upper-bounds a violation of safety in time. We report on a way to systematically tighten the lower bounds of service quality known of a region-adherent algorithm. Additionally, we present a technique - which we call hardening - for transforming a region-adherent algorithm into a region-adherent algorithm that compensates n+1 times as many faults as the input algorithm where n can freely be chosen. We explain how the technique works, what its underlying concepts are, its limitations, and prove its correctness. Finally, we compare the region adherence property of a hardened algorithm with its original, un-hardened counterpart by an example, thereby quantifying the beneficial impact of the transformation.

We present a new class of fault-tolerant distributed algorithms based on a concept which we call region adherence. A region-adherent algorithm upper-bounds the violation of safety due to faults in space. Region adherence counter-poses the concept of self-stabilization which upper-bounds a violation of safety in time. It turns out that region adherence is an orthogonal concept to self-stabilization. We give a formal definition of region-adherence that, intuitively, upper-bounds the reduction of the algorithm's service quality per fault. Then, we present a sample algorithm that exhibits region-adherent behavior and prove this property formally. Finally, we analyze the service quality of the sample algorithm via simulation and compare it to the worst-case behavior stated by the region adherence property.