Search

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.

Cyber-physical systems theory offers a powerful framework for modeling, analyzing, and designing real engineering systems integrating communication, control, and computation functionalities (the cyber part) within a natural and/or man-made system governed by the laws of physics (the physical part). New methodological developments in cyber-physical systems theory are required by traditional application domains such as manufacturing, transportation, and energy systems, which are currently experiencing significant and – to some extent – revolutionary changes to address the needs of our modern society. The goal of this position paper is to provide the cyber-physical systems community, and especially young researchers, a clear view on what are research directions worth pursuing motivated by the challenges posed by modern applications.

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.

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.

Model-based development is an important paradigm for developing cyber-physical systems (CPS). The underlying assumption is that the functional behavior of a model is related to the behavior of a more concretized model or the real system. A formal definition of such a relation is called conformance relation. There are a variety of conformance relations, and the question arises of how to select a conformance relation for the development of CPS. The contribution of this article is a survey of the definitions and algorithms of conformance relations for CPS. Additionally, the article compares several conformance relations and provides guidance on which relation to select for specific problems. Finally, we discuss how to select inputs for testing conformance.

In this paper, we provide a toolchain that facilitates the integration of formal verification techniques into model-based design. Applying verification tools to industrially relevant models requires three main ingredients: a formal model, a formal verification method, and a set of formal specifications. Our focus is on hybrid automata as the model and on reachability analysis as the method. Much progress has been made towards developing efficient and scalable reachability algorithms tailored to hybrid automata. However, it is not easy to encode rich formal specifications such that they can be interpreted by existing tools for reachability. Herein, we consider specifications expressed in pattern templates which are predefined properties with placeholders for state predicates. Pattern templates are close to the natural language and can be easily understood by both expert and non-expert users. We provide (i) formal definitions for selected patterns in the formalism of hybrid automata and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the property can be checked by off-the-shelf fully automated verification tools. We illustrate the workflow on an electro-mechanical brake use case.

In this experience report, we apply the hybrid verification toolsiSAT-ODE, Flow*, and S-TaLiRo to a case study consisting of an experimentalelectro-mechanical braking system. Starting from a Simulink closed-loopmodel, we describe the derivation of hybrid automaton models for plantand controller and give verifcation results for the different tools.

While requirements engineering has received considerable attention inacademia over the past years, formalization of requirements for physicallyinfluenced systems is still a difficult task in practice. In this paper, we giveformal representations of some typical requirement classes arising in theautomotive industry. We divide these patterns into three main classes:those mostly referring to properties of continuous signals, those mostlyreferring to discrete events and those referring to similarity to a referencesignal. We discuss these patterns on concrete examples from automotiveembedded systems, where specifications are used for test case generation.

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.

One defining characteristic of embedded software systems is the tight interaction with the context of the system, which gives rise to real-time constraints for the software. In this chapter, we focus on one relevant class of software: systems interacting with a physical context.

Stability is a very important property of feedback control systems. For linear feedback control systems, methods for proving or disproving system stability are well known. They basically amount to eigenvalue computations. For more general classes of feedback control systems, however, these methods are not applicable. A very general method is based on Lyapunov theory [7]. It uses a so-called Lyapunov function which can be regarded as generalized “energy function” of the system under investigation. If energy converges to zero over time then the system state will converge towards an equilibrium state. In the scope of the AVACS project,1 we are concerned with automatically proving hybrid system stability. In a first phase of the project, we focus on a special subclass of hybrid systems, namely piecewise affine hybrid systems. Hybrid systems contain both, discrete states and continuoustime dynamics. Piecewise affine hybrid systems require the continuous-time dynamics to be affine for each discrete state. A powerful method of verifying stability for such systems is based on extensions of Lyapunov theory, as proposed by Pettersson [9], Johansson et. al. [6] or Branicky [4]. These approaches still require system dependent inputs which could – up to now– only be provided by a human proof designer based on his or her intuition and expert knowledge of the problem domain. The work presented in this paper reports on our current status with respect to achieve full automatization of the stability verification task. The goal is to be able to prove stability of piecewise affine hybrid systems “by the push of a button” and without any further knowledge provided by a human user. In the future, we plan to extend and to complement the approach in order to cope with more general non-linear systems, possibly through approximation.

We propose a library based incremental design methodology for constructing hybrid controllers from a component library of models of hybrid controllers, such that global safety and stability properties are preserved. To this end, we propose hybrid interface specifications of components characterizing plant regions for which safety and stability properties are guaranteed, as well as exception mechanisms allowing safe and stability-preserving transfer of control whenever the plant evolves towards the boundary of controllable dynamics. We then propose a composition operator for constructing hybrid automata from a library of such pre-characterized components supported by compositional and automatable proofs of hybrid interface specifications.

We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.

Stability is an important system property. In this paper we examine the steps toward fully automated stability verification for a class of discrete-time hybrid systems. These systems are hybrid in the sense that they can have several modes with possibly different discrete-time dynamics. For systems with affine discrete-time dynamics in each mode, we employ a method that is based on Lyapunov theory and reduces the verification task to convex optimization. We detail the steps that are needed for automatic stability verification using this method: 1) choice of a state space partitioning 2) calculation of possible transitions between the different regions of the partitioning and 3) conversion of the problem into linear matrix inequalities, which can be solved through convex optimization. For steps 2) and 3) we present solutions that are suitable for full automation.

Self-stabilization is a novel method for achieving fault tolerance in distributed applications. A self-stabilizing algorithm will reach a legal set of states, regardless of the starting state or states adopted due to the effects of transient faults, infinite time. However, proving self-stabilization is a difficult task. In this paper, we present a method for showing self-stabilization of a class of non-silent distributed algorithms, namely orbitally self-stabilizing algorithms. An algorithm of this class is modeled as a hybrid feedback control system. We then employ the control theoretic methods of Poincare maps and Lyapunov functions to show convergence to an orbit cycle.

The verification of the self-stabilization property of a distributed algorithm is a complicated task. By exploiting certain analogies between self-stabilizing distributed algorithms and globally asymptotically stable feedback systems, techniques originally developed for the verification of feedback system stability can be adopted for the verification of self-stabilization of distributed algorithms. In this paper, we show how for a certain subclass of dynamic systems – namely piecewise affine hybrid systems – and distributed algorithms suitable to be modeled in terms of these dynamic systems, a proof of convergence can be obtain fully automatically. Together with some additional non-automated arguments, the complete proof of self-stabilization can be derived.