Search

Random ordinary differential equations (RODEs) are ordinary differential equations (ODEs) that contain a stochastic process in their vector field functions. They have been used for many years in a wide range of applications, but have been a shadow existence to stochastic differential equations (SDEs) despite being able to model a wider and often physically more adequate range of disturbances. In this article, we study the safety verification problem over both finite time horizons and the infinite time horizon for RODEs incorporating Wiener processes. Concretely, we investigate the ${p}$ -safety problem, where we identify the set of initial states from which the probability to satisfy safety specifications is at least ${p}$ . Based on identifying a set of sample paths whose probability measure is larger than ${p}$ , we propose a method of reducing stochastic reachability to adversary reachability of ODEs for solving the ${p}$ -safety problem over finite time horizons. This method permits an efficient lifting of reach-set computation methods for perturbed ODEs to RODEs. In this method, the ${p}$ -safety problem over finite time horizons is reduced to the problem of inner-approximating robust backward reachable sets for ODEs with time-varying perturbation inputs. We then extend the method to the ${p}$ -safety problem over the infinite time horizon. Finally, we demonstrate our method on several examples.

We study numerically the maximum $z$-matching problems on ensembles of bipartite random graphs. The $z$-matching problems describes the matching between two types of nodes, users and servers, where each server may serve up to $z$ users at the same time. By using a mapping to standard maximum-cardinality matching, and because for the latter there exists a polynomial-time exact algorithm, we can study large system sizes of up to $10^6$ nodes. We measure the capacity and the energy of the resulting optimum matchings. First, we confirm previous analytical results for bipartite regular graphs. Next, we study the finite-size behaviour of the matching capacity and find the same scaling behaviour as before for standard matching, which indicates the universality of the problem. Finally, we investigate for bipartite Erd\H{o}s-R\'enyi random graphs the saturability as a function of the average degree, i.e., whether the network allows as many customers as possible to be served, i.e. exploiting the servers in an optimal way. We find phase transitions between unsaturable and saturable phases. These coincide with a strong change of the running time of the exact matching algorithm, as well with the point where a minimum-degree heuristic algorithm starts to fail., Comment: 10 pages, 9 figures, 3 tables

This study develops a comparative, sociotechnical design perspective for interdisciplinary teams of social scientists and computer scientists. Sociotechnical design refers to identifying both technical and governance challenges and to understanding the ways in which the two types of problems affect and define each other. Approaching design as an open-ended, iterative process, the study develops a triple comparative perspective to problem finding and solutions: across two types of technological systems (the smart grid and connected and automated vehicles), three areas of societal implication and values (safety, equity, and privacy), and two continents (North America and Europe with a focus on the U.S. and Germany). The study then describes the implementation in an international collaboration of research and teaching. The collaborative experience and comparative research provide insights into the salience of the values across technological systems, portability of solutions across technological systems, and potential for policy harmonization across countries.

Ensuring safe behavior for automated vehicles in unregulated traffic areas poses a complex challenge for the industry. It is an open problem to provide scalable and certifiable solutions to this challenge. We derive a trajectory planner based on model predictive control which interoperates with a monitoring system for pedestrian safety based on cellular automata. The combined planner-monitor system is demonstrated on the example of a narrow indoor parking environment. The system features deterministic behavior, mitigating the immanent risk of black boxes and offering full certifiability. By using fundamental and conservative prediction models of pedestrians the monitor is able to determine a safe drivable area in the partially occluded and unstructured parking environment. The information is fed to the trajectory planner which ensures the vehicle remains in the safe drivable area at any time through constrained optimization. We show how the approach enables solving plenty of situations in tight parking garage scenarios. Even though conservative prediction models are applied, evaluations indicate a performant system for the tested low-speed navigation.

Autonomous vehicles may become an important part of traffic in the next few decades. One of the key factors that contribute to the acceptance of the technology is that the user can understand and to a certain degree predict the behaviour of the automation. One way to communicate the automation's intention and behaviour are graphical human-machine interfaces (HMIs). An online survey was conducted to evaluate five designs for HMIs for turning manoeuvres in automated vehicles. During the survey the participants rated the HMIs based on videos. The overall ratings don't show a clear favourite, however, a separation of the participants regarding their trust in automation and technical affinity indicate preferences regarding the preferred level of abstraction. Furthermore, 97% of the participants agreed that HMIs like the ones presented would help them gain or increase their trust in automated vehicles.

We study conflict situations that dynamically arise in traffic scenarios, where different agents try to achieve their set of goals and have to decide on what to do based on their local perception. We distinguish several types of conflicts for this setting. In order to enable modelling of conflict situations and the reasons for conflicts, we present a logical framework that adopts concepts from epistemic and modal logic, justification and temporal logic. Using this framework, we illustrate how conflicts can be identified and how we derive a chain of justifications leading to this conflict. We discuss how conflict resolution can be done when a vehicle has local, incomplete information, vehicle to vehicle communication (V2V) and partially ordered goals., In Proceedings CREST 2019, arXiv:1910.13641. arXiv admin note: substantial text overlap with arXiv:1905.11764

Emerging industrial platforms such as the Internet of Things (IoT), Industrial Internet (II) in the US and Industrie 4.0 in Europe have tremendously accelerated the development of new generations o...

Stochastic discrete-time systems, i.e., discrete-time dynamic systems subject to stochastic disturbances, are an essential modelling tool for many engineering systems, and reach-avoid analysis is able to guarantee safety (i.e., via avoiding unsafe sets) and progress (i.e., via reaching target sets). In this paper we study the reach-avoid problem of stochastic discrete-time systems over open (i.e., not bounded a priori) time horizons. The stochastic discrete-time system of interest is modeled by iterative polynomial maps with stochastic disturbances, and the problem addressed is to effectively compute an inner approximation of its p-reach-avoid set. The p-reach-avoid set collects those initial states that give rise to a bundle of trajectories which with probability being larger than p eventually hits a designated set of target states while remaining inside a set of safe states before the first hit. The computation of the p-reach-avoid set is first reduced to the computation of a corresponding strict p-super-level set and is then inner-approximated by solving a semi-definite programming problem obtained from a relaxation of the definition of the super-level set. Two examples demonstrate the proposed approach.

In this paper we propose a computational method based on semi-definite programming for synthesizing infinite-time reach-avoid sets in discrete-time polynomial systems. An infinite-time reach-avoid set is a set of initial states making the system eventually, i.e., within finite time enter the target set while remaining inside another specified (safe) set during each time step preceding the target hit. The reach-avoid set is first characterized equivalently as a strictly positive sub-level of a bounded value function, which in turn is shown to be a solution to a system of derived equations. The derived equations are further relaxed into a system of inequalities, which is encoded into semi-definite constraints based on the sum-of-squares decomposition for multivariate polynomials, such that the problem of synthesizing inner-approximations of the reach-avoid set can be addressed via solving a semi-definite programming problem. Two examples demonstrate the proposed approach.

Software updates are indispensable for the continuous development of Cyber Physical Systems (CPS): They allow for low-cost bug-fixing, fast adaptation to new or changing environments, or adding new functionality throughout the CPS’s life-cycle. Due to the urgent need for some safety-critical updates, their verification and validation may need to happen as fast as possible without loss of quality. For this reason, incremental checks targeting specifically the introduced changes and their impact on the system are essential as they speed up the validation process. In this paper, we introduce a concept for such an incremental verification for different types of updates by using contract-based design and verifying the integration of the introduced changes by checking their compliance with the contractually agreed assumptions and guarantees. We demonstrate our approach by applying two update types to an Adaptive Cruise Control (ACC) system and verifying the impact of the changes within the environment of the changed module(s).

The development of autonomous vehicles has gained a rapid pace. Along with the promising possibilities of such automated systems, the question of how to ensure their safety arises. With increasing levels of automation the need for fail-operational systems, not relying on a back-up driver, poses new challenges in system design. In this paper we propose a lightweight architecture addressing the challenge of a verifiable, fail-safe safety implementation for trajectory planning. It offers a distributed design and the ability to comply with the requirements of ISO26262, while avoiding an overly redundant setup. Furthermore, we show an example with low-level prediction models applied to a real world situation.

Acta informatica xx, xx-xx (2020). doi:10.1007/s00236-020-00374-7, Published by Springer, New York, NY

We present an integrated method for safety assessment of automated driving systems which covers the aspects of functional safety and safety of the intended functionality (SOTIF), including identification and quantification of hazardous scenarios. The proposed method uses and combines established exploration and analytical tools for hazard analysis and risk assessment in the automotive domain, while adding important enhancements to enable their applicability to the uncharted territory of safety analyses for automated driving. The method is tailored to support existing safety processes mandated by the standards ISO 26262 and ISO/PAS 21448 and complements them where necessary. It has been developed in close cooperation with major German automotive manufacturers and suppliers within the PEGASUS project (https://www.pegasusprojekt.de/en). Practical evaluation has been carried out by applying the method to the PEGASUS Highway-Chauffeur, a conceptual automated driving function considered as a common reference system within the project.

Advances in Vehicular Cyber-Physical Systems (VCPS) are the primary enablers of the shift from no automation to fully autonomous vehicles (AVs). One of the impacts of this shift is to develop safe AVs in which most or all of the functions of the human driver are replaced with an intelligent system. However, while some progress has been made in equipping AVs with advanced AI capabilities, VCPS designers are still faced with the challenge of designing trustworthy AVs that are in sync with the unpredictable behaviours of humans. In order to address this challenge, we present a model that describes how a Human Ambassador component can be integrated into the overall design of a new generation of VCPS. A scenario is presented to demonstrate how the model can work in practice. Formalisation and co-simulation challenges associated with integrating the Human Ambassador component and future work we are undertaking are also discussed.

Emerging smart technologies add elements of intelligence, cooperation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes. Hybrid automata, in their various flavours, have been suggested as a formal model accurately capturing CPS dynamics and thus facilitating exhaustive behavioural analysis of interacting CPSes with mathematical rigour.

This paper presents a combined Nonlinear Model Predictive Control (NMPC) for position and velocity tracking of underactuated surface vessels, and collision avoidance of static and dynamic objects into a single control scheme with sideslip angle compensation and environmental disturbances counteraction. A three-degree-of-freedom (3-DOF) dynamic model is used with only two control variables: namely, surge force and yaw moment. External environmental forces are considered as constant or slowly varying disturbances with respect to the inertial frame, and hence nonlinear for the body frame of the vessel. Nonlinear disturbance observer (NDO) is used to estimate these disturbances in order to be fed into the prediction model and enhance the robustness of the controller. A nonlinear optimization problem is formulated to minimize the deviation of the vessel states from a time varying reference generated over a finite horizon by a virtual vessel. Sideslip angle is considered in the cost function formulation to account for tracking error caused by the transverse external force in the absence of sway control force. Collision avoidance is embedded into the trajectory tracking control problem as a time-varying nonlinear constraint of position states to account for static and dynamic obstacles. MATLAB simulations are used to assess the validity of the proposed technique.

Delay differential equations (DDEs) play an important role in the modeling of dynamic processes. Delays arise in contemporary control schemes like networked distributed control and can cause deterioration of control performance, invalidating both stability and safety properties. This induces an interest in DDE especially in the area of modeling and verification of embedded control. In this article, we present an approach aiming at automatic safety verification of a simple class of DDEs against requirements expressed in a linear-time temporal logic. As requirements specification language, we exploit metric interval temporal logic (MITL) with a continuous-time semantics evaluating signals over metric spaces. We employ an over-approximation method based on interval Taylor series to enclose the solution of the DDE and thereby reduce the continuous-time verification problem for MITL formulae to a discrete-time problem over sequences of Taylor coefficients. We encode sufficient conditions for satisfaction as SMT formulae over polynomial arithmetic and use the iSAT3 SMT solver in its bounded model-checking mode for discharging the resulting proof obligations, thus proving satisfaction of time-bounded MITL specifications by the trajectories induced by a DDE. In contrast to our preliminary work in [44], we can verify arbitrary time-bounded MITL formulae, including nesting of modalities, rather than just invariance properties.

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year’s edition of the competition. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Spring 2019.

Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it consequently is omnipresent in safety-critical domains, there is an increasing interest in the safety verification of systems modelled by Delay Differential Equations (DDEs). In this paper, we leverage qualitative guarantees for the existence of an exponentially decreasing estimation on the solutions to DDEs as established in classical stability theory, and present a quantitative method for constructing such delay-dependent estimations, thereby facilitating a reduction of the verification problem over an unbounded temporal horizon to a bounded one. Our technique builds on the linearization technique of nonlinear dynamics and spectral analysis of the linearized counterparts. We show experimentally on a set of representative benchmarks from the literature that our technique indeed extends the scope of bounded verification techniques to unbounded verification tasks. Moreover, our technique is easy to implement and can be combined with any automatic tool dedicated to bounded verification of DDEs.