Visible to the public BiblioConflict Detection Enabled

2019-09-27
Janos Sztipanovits, Xenofon Koutsoukos, Gabor Karsai, Shankar Sastry, Claire Tomlin, Werner Damm, Martin Fränzle, Jochem Rieger, Alexander Pretschner, Frank Köster.  2019.  Science of design for societal-scale cyber-physical systems: challenges and opportunities. Cyber-Physical Systems. 5:145-172.

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 of Cyber-Physical Systems (CPS) that integrate humans and human organizations (H-CPS) with physical and computation processes and extend to societal-scale systems such as traffic networks, electric grids, or networks of autonomous systems where control is dynamically shifted between humans and machines. Although such societal-scale CPS can potentially affect many aspect of our lives, significant societal strains have emerged about the new technology trends and their impact on how we live. Emerging tensions extend to regulations, certification, insurance, and other societal constructs that are necessary for the widespread adoption of new technologies. If these systems evolve independently in different parts of the world, they will ‘hard-wire’ the social context in which they are created, making interoperation hard or impossible, decreasing reusability, and narrowing markets for products and services. While impacts of new technology trends on social policies have received attention, the other side of the coin – to make systems adaptable to social policies – is nearly absent from engineering and computer science design practice. This paper focuses on technologies that can be adapted to varying public policies and presents (1) hard problems and technical challenges and (2) some recent research approaches and opportunities. The central goal of this paper is to discuss the challenges and opportunities for constructing H-CPS that can be parameterized by social context. The focus in on three major application domains: connected vehicles, transactive energy systems, and unmanned aerial vehicles.Abbreviations: CPS: Cyber-physical systems; H-CPS: Human-cyber-physical systems; CV: Connected vehicle; II: Industrial Internet; IoT: Internet of Things

2019-08-28
Margaret Chapman, Jonathan Lacotte, Aviv Tamar, Donggun Lee, Kevin M. Smith, Victoria Cheng, Jamie Fisac, Susmit Jha, Marco Pavone, Claire J. Tomlin.  2019.  A Risk-Sensitive Finite-Time Reachability Approach for Safety of Stochastic Dynamic Systems. American Control Conference.

A classic reachability problem for safety of dynamic systems is to compute the set of initial states from which the state trajectory is guaranteed to stay inside a given constraint set over a given time horizon. In this paper, we leverage existing theory of reachability analysis and risk measures to devise a risk-sensitive reachability approach for safety of stochastic dynamic systems under non-adversarial disturbances over a finite time horizon. Specifically, we first introduce the notion of a risk-sensitive safe set as a set of initial states from which the risk of large constraint violations can be reduced to a required level via a control policy, where risk is quantified using the Conditional Value-at-Risk (CVaR) measure. Second, we show how the computation of a risk-sensitive safe set can be reduced to the solution to a Markov Decision Process (MDP), where cost is assessed according to CVaR. Third, leveraging this reduction, we devise a tractable algorithm to approximate a risk-sensitive safe set, and provide theoretical arguments about its correctness. Finally, we present a realistic example inspired from stormwater catchment design to demonstrate the utility of risk-sensitive reachability analysis. In particular, our approach allows a practitioner to tune the level of risk sensitivity from worst-case (which is typical for Hamilton-Jacobi reachability analysis) to risk-neutral (which is the case for stochastic reachability analysis).

Margaret Chapman, Kevin M. Smith, David L Freyberg, Victoria Cheng, Donggun Lee, Claire Tomlin.  2018.  Reachability Analysis as a Design Tool for Stormwater Systems: Towards Planning in the Presence of Stochastic Surface Runoff. IEEE Conference on Technologies for Sustainability (SusTech).

Stormwater infrastructure is required to safely manage uncertain precipitation events of varying intensity, while protecting natural ecosystems, under restricted financial budgets. In practice, candidate designs for stormwater detention or retention systems are commonly evaluated assuming that a given system operates independently from nearby systems and is initially empty prior to an extreme storm event. In recent work, we demonstrate the use of a control-theoretic method, called reachability analysis, to provide a more realistic design-phase indicator of system performance [1]. In particular, reachability analysis predicts the response of a dynamically-coupled stormwater storage network to a deterministic storm event under a wide range of initial conditions simultaneously [1]. The outcomes of this analysis can be viewed as measures of system robustness that inform the evaluation of safety-critical design choices [1]. Here we discuss how to extend the recent work to incorporate the stochastic nature of surface runoff. We represent surface runoff as a random disturbance to a dynamic system model of a stormwater storage network. Using a probability distribution of surface runoff derived from a Monte Carlo method, we apply an existing algorithm [2] for stochastic reachability analysis to the problem of designing robust stormwater storage systems. We discuss particular advantages and disadvantages of using stochastic reachability analysis, deterministic reachability analysis, or random sampling to assess system robustness.

2019-08-21
Bai Xue, Martin Frönzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran.  2019.  Probably Approximate Safety Verification of Hybrid Dynamical Systems. 21st International Conference on Formal Engineering Methods.

In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems over the infinite time horizon subject to perturbation inputs. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

Anirudh Unni, Benedikt Kretzmeyer, Klas Ihme, Frank Köster, Meike Jipp, Jochem W. Rieger.  2018.  Demonstrating brain-level interactions between working memory load and frustration while driving using functional near-infrared spectroscopy. 2nd International Neuroergonomics Conference.

Mental workload is a popular concept in ergonomics as it provides an intuitive explanation why exceedingly cognitive task demands result in a decrease in task performance and increase the risk of fatal incidents while driving. At the same time, affective states such as frustration, also play a role in traffic safety as they increase the tendency for speedy and aggressive driving and may even degrade cognitive processing capacities. To reduce accidents due to dangerous effects of degraded cognitive processing capacities and affective biases causing human errors, it is necessary to continuously assess multiple user states simultaneously to better understand potential interactions. In two previous studies, we measured brain activity with functional near-infrared spectroscopy (fNIRS) for separate brain based prediction of working memory load (WML) (Unni et al., 2017) and frustration levels (Ihme et al. submitted) while driving. Here, we report results from a study designed to predict simultaneously manipulated WML and frustration using data driven machine learning approaches from whole-head fNIRS brain activation measurements. 

Alexander Trende, Anirudh Unni, Lars Weber, Jochem Rieger, Andreas Lüdtke.  2019.  An investigation into human-autonomous vs. human-human vehicle interaction in time-critical situations. 12th Pervasive Technologies Related to Assistive Environments Conference. :303-304.

We performed a driving simulator study to investigate merging decisions with respect to an interaction partner in time-critical situations. The experimental paradigm was a two-alternative forced choice, where the subjects could choose to merge before human vehicles or highly automated vehicles (HAV). Under time pressure, subjects showed a significantly higher gap acceptance during merging situations when interacting with HAV. This confirmed our original hypothesis that when interacting with HAV, drivers would exploit the HAV's technological advantages and defensive programming in time-critical situations.
 

Janos Sztipanovits, Xenofon Koutsoukos, Gabor Karsai, Shankar Sastry, Claire Tomlin, Werner Damm, Martin Frönzle, Jochem Rieger, Alexander Pretschner, Frank Köster.  2019.  Science of design for societal-scale cyber-physical systems: challenges and opportunities. Cyber-Physical Systems. 5:145-172.

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 of Cyber-Physical Systems (CPS) that integrate humans and human organizations (H-CPS) with physical and computation processes and extend to societal-scale systems such as traffic networks, electric grids, or networks of autonomous systems where control is dynamically shifted between humans and machines. Although such societal-scale CPS can potentially affect many aspect of our lives, significant societal strains have emerged about the new technology trends and their impact on how we live. Emerging tensions extend to regulations, certification, insurance, and other societal constructs that are necessary for the widespread adoption of new technologies. If these systems evolve independently in different parts of the world, they will ‘hard-wire’ the social context in which they are created, making interoperation hard or impossible, decreasing reusability, and narrowing markets for products and services. While impacts of new technology trends on social policies have received attention, the other side of the coin – to make systems adaptable to social policies – is nearly absent from engineering and computer science design practice. This paper focuses on technologies that can be adapted to varying public policies and presents (1) hard problems and technical challenges and (2) some recent research approaches and opportunities. The central goal of this paper is to discuss the challenges and opportunities for constructing H-CPS that can be parameterized by social context. The focus in on three major application domains: connected vehicles, transactive energy systems, and unmanned aerial vehicles.Abbreviations: CPS: Cyber-physical systems; H-CPS: Human-cyber-physical systems; CV: Connected vehicle; II: Industrial Internet; IoT: Internet of Things

Julian Schindler, Frank Köster.  2016.  A Model-Based Approach for Performing Successful Multi-Driver Scenarios. Driving Simulation Conference.

When designing driving simulator studies, sometimes high efforts have to be spent to make them successful. Some drivers may not behave as desired, leading to situations unforeseen by the developers. When looking at multi-driver studies, where multiple drivers need to interact with each other in one virtual environment, the probability of performing a successful study is even lower, as the behaviour of the human drivers cannot be fully controlled. While [Oel15b] already proposed guidelines for the creation of such scenarios, this paper describes how the probability of success can be monitored and even enhanced during scenario execution. Therefore, it describes an approach where the probability of success is modelled and where the scenario is dynamically adapted to provide higher rates of success.
 

Jakob Scheunemann, Anirudh Unni, Klas Ihme, Meike Jipp, Jochem W. Rieger.  2019.  Demonstrating Brain-Level Interactions Between Visuospatial Attentional Demands and Working Memory Load While Driving Using Functional Near-Infrared Spectroscopy. Frontiers in Human Neuroscience. 12

Driving is a complex task concurrently drawing on multiple cognitive resources. Yet, there is a lack of studies investigating interactions at the brain-level among different driving subtasks in dual-tasking. This study investigates how visuospatial attentional demands related to increased driving difficulty interacts with different working memory load (WML) levels at the brain level. Using multichannel whole-head high density functional near-infrared spectroscopy (fNIRS) brain activation measurements, we aimed to predict driving difficulty level, both separate for each WML level and with a combined model. Participants drove for approximately 60 min on a highway with concurrent traffic in a virtual reality driving simulator. In half of the time, the course led through a construction site with reduced lane width, increasing visuospatial attentional demands. Concurrently, participants performed a modified version of the n-back task with five different WML levels (from 0-back up to 4-back), forcing them to continuously update, memorize, and recall the sequence of the previous 'n' speed signs and adjust their speed accordingly. Using multivariate logistic ridge regression, we were able to correctly predict driving difficulty in 75.0% of the signal samples (1.955 Hz sampling rate) across 15 participants in an out-of-sample cross-validation of classifiers trained on fNIRS data separately for each WML level. There was a significant effect of the WML level on the driving difficulty prediction accuracies [range 62.2-87.1%; χ2(4) = 19.9, p < 0.001, Kruskal-Wallis H test] with highest prediction rates at intermediate WML levels. On the contrary, training one classifier on fNIRS data across all WML levels severely degraded prediction performance (mean accuracy of 46.8%). Activation changes in the bilateral dorsal frontal (putative BA46), bilateral inferior parietal (putative BA39), and left superior parietal (putative BA7) areas were most predictive to increased driving difficulty. These discriminative patterns diminished at higher WML levels indicating that visuospatial attentional demands and WML involve interacting underlying brain processes. The changing pattern of driving difficulty related brain areas across WML levels could indicate potential changes in the multitasking strategy with level of WML demand, in line with the multiple resource theory.

Himanshu Neema, Janos Sztipanovits, Cornelius Steinbrink, Thomas Raub, Bastian Cornelsen, Sebastian Lehnhoff.  2019.  Simulation Integration Platforms for Cyber-physical Systems. Workshop on Design Automation for Cyber-Physical Systems and Internet-of-Things. :10–19.

Simulation-based analysis is essential in the model-based design process of Cyber-Physical Systems (CPS). Since heterogeneity is inherent to CPS, virtual prototyping of CPS designs and the simulation of their behavior in various environments typically involve a number of physical and computation/communication domains interacting with each other. Affordability of the model-based design process makes the use of existing domain-specific modeling and simulation tools all but mandatory. However, this pressure establishes the requirement for integrating the domain-specific models and simulators into a semantically consistent and efficient system-of-system simulation. The focus of the paper is the interoperability of popular integration platforms supporting heterogeneous multi-model simulations. We examine the relationship among three existing platforms: the High-Level Architecture (HLA)-based CPS Wind Tunnel (CPSWT), MOSAIK, and the Functional Mockup Unit (FMU). We discuss approaches to establish interoperability and present results of ongoing work in the context of an example.

Karsten Lemmer, Werner Damm, Janos Stzipanovits, Shankar Sastry, Claire Tomlin, Frank Köster, Meike Jipp.  2019.  Societal and Technological Research Challenges for Highly Automated Road Transportation Systems in Germany and the US: Diversities and Synergy Potentials. Workshop on Societal and Technological Research Challenges for Highly Automated Road Transportation Systems in Germany and the US: Diversities and Synergy Potentials.
Severin Kacianka, Alexander Pretschner.  2018.  Understanding and Formalizing Accountability for Cyber-Physical Systems. IEE International Conference on Systems, Man, and Cybernetics. :3165–3170.

Accountability is the property of a system that enables the uncovering of causes for events and helps understand who or what is responsible for these events. Definitions and interpretations of accountability differ; however, they are typically expressed in natural language that obscures design decisions and the impact on the overall system. This paper presents a formal model to express the accountability properties of cyber-physical systems. To illustrate the usefulness of our approach, we demonstrate how three different interpretations of accountability can be expressed using the proposed model and describe the implementation implications through a case study. This formal model can be used to highlight context specific-elements of accountability mechanisms, define their capabilities, and express different notions of accountability. In addition, it makes design decisions explicit and facilitates discussion, analysis and comparison of different approaches.

Severin Kacianka, Amjad Ibrahim, Alexander Pretschner, Alexander Trende, Andreas Lüdtke.  2019.  Extending Causal Models from Machines into Humans. 4th Causation, Responsibility, & Explanations in Science & Technology Workshop.

Causal Models are increasingly suggested as a mean to reason about the behavior of cyber-physical systems in socio-technical contexts. They allow us to analyze courses of events and reason about possible alternatives. Until now, however, such reasoning is confined to the technical domain and limited to single systems or at most groups of systems. The humans that are an integral part of any such socio-technical system are usually ignored or dealt with by “expert judgment”. We show how a technical causal model can be extended with models of human behavior to cover the complexity and interplay between humans and technical systems. This integrated socio-technical causal model can then be used to reason not only about actions and decisions taken by the machine, but also about those taken by humans interacting with the system. In this paper we demonstrate the feasibility of merging causal models about machines with causal models about humans and illustrate the usefulness of this approach with a highly automated vehicle example.

Klas Ihme, Anirudh Unni, Meng Zhang, Jochem W. Rieger, Meike Jipp.  2018.  Recognizing frustration of drivers from face video recordings and brain activation measurements with functional near-infrared spectroscopy. Frontiers in Human Neuroscience. 12

Experiencing frustration while driving can harm cognitive processing, result in aggressive behavior and hence negatively influence driving performance and traffic safety. Being able to automatically detect frustration would allow adaptive driver assistance and automation systems to adequately react to a driver’s frustration and mitigate potential negative consequences. To identify reliable and valid indicators of driver’s frustration, we conducted two driving simulator experiments. In the first experiment, we aimed to reveal facial expressions that indicate frustration in continuous video recordings of the driver’s face taken while driving highly realistic simulator scenarios in which frustrated or non-frustrated emotional states were experienced. An automated analysis of facial expressions combined with multivariate logistic regression classification revealed that frustrated time intervals can be discriminated from non-frustrated ones with accuracy of 62.0% (mean over 30 participants). A further analysis of the facial expressions revealed that frustrated drivers tend to activate muscles in the mouth region (chin raiser, lip pucker, lip pressor). In the second experiment, we measured cortical activation with almost whole-head functional near-infrared spectroscopy (fNIRS) while participants experienced frustrating and non-frustrating driving simulator scenarios. Multivariate logistic regression applied to the fNIRS measurements allowed us to discriminate between frustrated and non-frustrated driving intervals with higher accuracy of 78.1% (mean over 12 participants). Frustrated driving intervals were indicated by increased activation in the inferior frontal, putative premotor and occipito-temporal cortices. Our results show that facial and cortical markers of frustration can be informative for time resolved driver state identification in complex realistic driving situations. The markers derived here can potentially be used as an input for future adaptive driver assistance and automation systems that detect driver frustration and adaptively react to mitigate it.

Amjad Ibrahim, Simon Rehwald, Alexander Pretschner.  2019.  Efficiently Checking Actual Causality with SAT Solving. Lecture Notes of the 2018 Marktoberdorf Summer school on Software Engineering. To Appear..

Recent formal approaches towards causality have made the concept ready for incorporation into the technical world. However, causality reasoning is computationally hard; and no general algorithmic approach exists that efficiently infers the causes for effects. Thus, checking causality in the context of complex, multi-agent, and distributed socio-technical systems is a significant challenge. Therefore, we conceptualize an intelligent and novel algorithmic approach towards checking causality in acyclic causal models with binary variables, utilizing the optimization power in the solvers of the Boolean Satisfiability Problem (SAT). We present two SAT encodings, and an empirical evaluation of their efficiency and scalability. We show that causality is computed efficiently in less than 5 seconds for models that consist of more than 4000 variables.

Amjad Ibrahim, Severin Kacianka, Alexander Pretschner, Charles Hartsell, Gabor Karsai.  2019.  Practical Causal Models for Cyber-Physical Systems. NASA Formal Methods. :211–227.

Unlike faults in classical systems, faults in Cyber-Physical Systems will often be caused by the system's interaction with its physical environment and social context, rendering these faults harder to diagnose. To complicate matters further, knowledge about the behavior and failure modes of a system are often collected in different models. We show how three of those models, namely attack trees, fault trees, and timed failure propagation graphs can be converted into Halpern-Pearl causal models, combined into a single holistic causal model, and analyzed with actual causality reasoning to detect and explain unwanted events. Halpern-Pearl models have several advantages over their source models, particularly that they allow for modeling preemption, consider the non-occurrence of events, and can incorporate additional domain knowledge. Furthermore, such holistic models allow for analysis across model boundaries, enabling detection and explanation of events that are beyond a single model. Our contribution here delineates a semi-automatic process to (1) convert different models into Halpern-Pearl causal models, (2) combine these models into a single holistic model, and (3) reason about system failures. We illustrate our approach with the help of an Unmanned Aerial Vehicle case study.

Hauer, Florian, Raphael Stern, Alexander Pretschner.  2019.  Selecting Flow Optimal System Parameters for Automated Driving Systems . 22nd International Conference on Intelligent Transportation Systems.

Driver assist features such as adaptive cruise control (ACC) and highway assistants are becoming increasingly prevalent on commercially available vehicles. These systems are typically designed for safety and rider comfort. However, these systems are often not designed with the quality of the overall traffic flow in mind. For such a system to be beneficial to the traffic flow, it must be string stable and minimize the inter-vehicle spacing to maximize throughput, while still being safe. We propose a methodology to select autonomous driving system parameters that are both safe and string stable using the existing control framework already implemented on commercially available ACC vehicles. Optimal parameter values are selected via model-based optimization for an example highway assistant controller with path planning.

Sven Hallerbach, Yiqun Xia, Ulrich Eberle, Frank Köster.  2018.  Simulation-based Identification of Critical Scenarios for Cooperative and Automated Vehicles. WCX World Congress Experience.

One of the major challenges for the automotive industry will be the release and validation of cooperative and automated vehicles. The immense driving distance that needs to be covered for a conventional validation process requires the development of new testing procedures. Further, due to limited market penetration in the beginning, the driving behavior of other human traffic participants, regarding a mixed traffic environment, will have a significant impact on the functionality of these vehicles.In this paper, a generic simulation-based toolchain for the model-in-the-loop identification of critical scenarios will be introduced. The proposed methodology allows the identification of critical scenarios with respect to the vehicle development process. The current development status of cooperative and automated vehicle determines the availability of testable simulation models, software, and components.The identification process is realized by a coupled simulation framework. A combination of a vehicle dynamics simulation that includes a digital prototype of the cooperative and automated vehicle, a traffic simulation that provides the surrounding environment, and a cooperation simulation including cooperative features, is used to establish a suitable comprehensive simulation environment. The behavior of other traffic participants is considered in the traffic simulation environment.The criticality of the scenarios is determined by appropriate metrics. Within the context of this paper, both standard safety metrics and newly developed traffic quality metrics are used for evaluation. Furthermore, we will show how the use of these new metrics allows for investigating the impact of cooperative and automated vehicles on traffic. The identified critical scenarios are used as an input for X-in-the-Loop methods, test benches, and proving ground tests to achieve an even more precise comparison to real-world situations. As soon as the vehicle development process is in a mature state, the digital prototype becomes a “digital twin” of the cooperative and automated vehicle.

Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, Bai Xue.  2019.  Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations. 31st International Conference on Computer Aided Verification. 11561:650-669.

Delayed coupling between state variables occurs regularly in technical dynamic systems, especially embedded control. As it consequently is omnipresent in safety-critical domains, there is an increasing interest in the safety verifications of systems modeled 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 non-linear 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.

Werner Damm, Martin Fränzle, Andreas Lüdtke, Jochem W. Rieger, Alexander Trende, Anirudh Unni.  2019.  Integrating Neurophysiological Sensors and Driver Models for Safe and Performant Automated Vehicle Control in Mixed Traffic. Workshop on Human Factors in Intelligent Vehicles.

In the future, mixed traffic Highly Automated Vehicles (HAV) will have to resolve interactions with human operated traffic. A particular problem for HAVs is the detection of human states influencing safety, critical decisions, and driving behavior of humans. We demonstrate the value proposition of neurophysiological sensors and driver models for optimizing performance of HAVs under safety constraints in mixed traffic applications.

Werner Damm, Martin Fränzle, Willem Hagemann, Paul Kröger, Astrid Rakow.  2019.  Justification Based Reasoning in Dynamic Conflict Resolution. 4th Workshop on Formal Reasoning about Causation, Responsibility, and Explanations in Science and Technology.

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.