Biblio

Filters: Author is Martin Fränzle  [Clear All Filters]
2021-08-11
2021-08-13
2021-08-12
Klaus Bengler, Bianca Biebl, Werner Damm, Martin Fränzle, Willem Hagemann, Moritz Held, Klas Ihme, Severin Kacianka, Sebastian Lehnhoff, Andreas Luedtke et al..  2021.  A Metamodel of Human Cyber Physical Systems. Working Document of the PIRE Project on Assuring Individual, Social, and Cultural Embeddedness of Autonomous Cyber-Physical Systems (ISCE-ACPS). :41.
2020-10-12
2020-10-01
Sebastian vom Dorff, Bert Böddeker, Maximilian Kneissl, Martin Fränzle.  2020.  A fail-safe architecture for automated driving. 23rd Conference on Design, Automation and Test in Europe. :828-833.

DATE is a leading international event providing unique networking opportunities, bringing together designers and design automation users, researchers and vendors, as well as specialists in hardware and software design, test and manufacturing of electronic circuits and systems.

2020-10-12
Martin Fränzle, Paul Kröger.  2020.  Guess what I’m doing! Rendering formal verification methods ripe for the era of interacting intelligent systems. 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation.
Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov, Bican Xia.  2020.  Safety verification for random ordinary differential equations. Proceedings of EMSOFT 2020: International Conference on Embedded Software.
2020-10-01
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan.  2020.  Indecision and delays are the parents of failure—taming them algorithmically by synthesizing delay-resilient control. Acta Informatica.

The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and adding an appropriate winning condition permits to specify desirable behavior. The classical model here is the positional game, where both players can (fully or partially) observe the current position in the game graph, which in turn is indicative of their mutual current states. In practice, neither sensing and actuating the environment through physical devices nor data forwarding to and from the controller and signal processing in the controller are instantaneous. The resultant delays force the controller to draw decisions before being aware of the recent history of a play and to submit these decisions well before they can take effect asynchronously. It is known that existence of a winning strategy for the controller in games with such delays is decidable over finite game graphs and with respect to ω-regular objectives. The underlying reduction, however, is impractical for non-trivial delays as it incurs a blow-up of the game graph which is exponential in the magnitude of the delay. For safety objectives, we propose a more practical incremental algorithm successively synthesizing a series of controllers handling increasing delays and reducing the game-graph size in between. It is demonstrated using benchmark examples that even a simplistic explicit-state implementation of this algorithm outperforms state-of-the-art symbolic synthesis algorithms as soon as non-trivial delays have to be handled. We furthermore address the practically relevant cases of non-order-preserving delays and bounded message loss, as arising in actual networked control, thereby considerably extending the scope of regular game theory under delay.

Björn Koopmann, Stefan Puch, Günter Ehmen, Martin Fränzle.  2020.  Cooperative Maneuvers of Highly Automated Vehicles at Urban Intersections: A Game-theoretic Approach. 6th International Conference on Vehicle Technology and Intelligent Transport Systems.

In this paper, we propose an approach how connected and highly automated vehicles can perform cooperative maneuvers such as lane changes and left-turns at urban intersections where they have to deal with human-operated vehicles and vulnerable road users such as cyclists and pedestrians in so-called mixed traffic. In order to support cooperative maneuvers the urban intersection is equipped with an intelligent controller which has access to different sensors along the intersection to detect and predict the behavior of the traffic participants involved. Since the intersection controller cannot directly control all road users and – not least due to the legal situation – driving decisions must always be made by the vehicle controller itself, we focus on a decentralized control paradigm. In this context, connected and highly automated vehicles use some carefully selected game theory concepts to make the best possible and clear decisions about cooperative maneuvers. The aim is to improve traffic efficiency while maintaining road safety at the same time. Our first results obtained with a prototypical implementation of the approach in a traffic simulation are promising.

Bai Xue, Martin Fränzle, Naijun Zhan.  2020.  Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Transactions on Automatic Control. 65(4):1468-1483.

In this paper, we propose a convex programming based method to address a long-standing problem of inner-approximating backward reachable sets of state-constrained polynomial systems subject to time-varying uncertainties. The backward reachable set is a set of states, from which all trajectories starting will surely enter a target region at the end of a given time horizon without violating a set of state constraints in spite of the actions of uncertainties. It is equal to the zero sublevel set of the unique Lipschitz viscosity solution to a Hamilton-Jacobi partial differential equation (HJE). We show that inner approximations of the backward reachable set can be formed by zero sublevel sets of its viscosity supersolutions. Consequently, we reduce the inner-approximation problem to a problem of synthesizing polynomial viscosity supersolutions to this HJE. Such a polynomial solution in our method is synthesized by solving a single semidefinite program. We also prove that polynomial solutions to the formulated semidefinite program exist and can produce a convergent sequence of inner approximations to the interior of the backward reachable set in measure under appropriate assumptions. This is the main contribution of this paper. Several illustrative examples demonstrate the merits of our approach.

Alexander Trende, Franziska Roesner, Cornelia Schmidt, Martin Fränzle.  2020.  Improving the detection of user uncertainty in automated overtaking maneuvers by combining contextual, physiological and individualized user data. International Conference on Human-Computer Interaction.

Highly automated driving will be a novel experience for many users and may cause uncertainty and discomfort for them. An efficient real-time detection of user uncertainty during automated driving may trigger adaptation strategies, which could enhance the driving experience and subsequently the acceptance of highly automated driving. In this study, we compared three different models to classify a user’s uncertainty regarding an automated vehicle’s capabilities and traffic safety during overtaking maneuvers based on experimental data from a driving-simulator study. By combining physiological, contextual and user-specific data, we trained three different deep neural networks to classify user uncertainty during overtaking maneuvers on different sets of input features. We evaluated the models based on metrics like the classification accuracy and F1 Scores. For a purely context-based model, we used features such as the Time-Headway and Time-To-Collision of cars on the opposing lane. We demonstrate how the addition of user heart rate and related physiological features can improve the classification accuracy compared to a purely context-based uncertainty model. The third model included user-specific features to account for inter-user differences regarding uncertainty in highly automated vehicles. We argue that a combination of physiological, contextual and user-specific information is important for an effectual uncertainty detection that accounts for inter-user differences.

2021-08-11
Sulayman K. Sowe, Martin Fränzle, Jan-Patrick Osterloh, Alexander Trende, Lars Weber, Andreas Lüdtke.  2020.  Challenges for Integrating Humans into Vehicular Cyber-Physical Systems. Software Engineering and Formal Methods. 12226:20–26.
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.
Martin Fränzle, Paul Kröger.  2020.  Guess What I'm Doing! - Rendering Formal Verification Methods Ripe for the Era of Interacting Intelligent Systems. Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III. 12478:255-272.
Birte Kramer, Christian Neurohr, Matthias Büker, Eckard Böde, Martin Fränzle, Werner Damm.  2020.  Identification and Quantification of Hazardous Scenarios for Automated Driving. Model-Based Safety and Assessment. :163–178.
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.
2019-08-21
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. IEEE Intelligent Vehicles Symposium.

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.

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-21
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.

2020-10-01
Martin Fränzle, Mingshuai Chen, Paul Kröger.  2019.  In memory of Oded Maler: automatic reachability analysis of hybrid-state automata. ACM SIGLOG News. 6(1)

Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with automata capturing switching behavior. Since the introduction of the computational model more than a quarter of a century ago [Maler et al. 1992], its algorithmic verification has been an area of intense research. Within this note, which is dedicated to Oded Maler (1957--2018) as one of the inventors of the model, we are trying to delineate major lines of attack to the reachability problem for hybrid automata. Due to its relation to system safety, the reachability problem is a prototypical verification problem for hybrid discrete-continuous system dynamics.

Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle.  2019.  Robust invariant sets generation for state-constrained perturbed polynomial systems. 22nd ACM International Conference on Hybrid Systems: Computation and Control.

In this paper we study the problem of computing robust invariant sets for state-constrained perturbed polynomial systems within the Hamilton-Jacobi reachability framework. A robust invariant set is a set of states such that every possible trajectory starting from it never violates the given state constraint, irrespective of the actual perturbation. The main contribution of this work is to describe the maximal robust invariant set as the zero level set of the unique Lipschitz-continuous viscosity solution to a Hamilton-Jacobi-Bellman (HJB) equation. The continuity and uniqueness property of the viscosity solution facilitates the use of existing numerical methods to solve the HJB equation for an appropriate number of state variables in order to obtain an approximation of the maximal robust invariant set. We furthermore propose a method based on semi-definite programming to synthesize robust invariant sets. Some illustrative examples demonstrate the performance of our methods.

2021-08-11
Werner Damm, Martin Fränzle, Willem Hagemann, Paul Kröger, Astrid Rakow.  2019.  Dynamic Conflict Resolution Using Justification Based Reasoning. Proceedings of the 4th Workshop on Formal Reasoning about Causation, Responsibility, and Explanations in Science and Technology. 308:47–65.
2020-10-12
2019-08-21
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.