With the increasing level of automation in road vehicles, the traditional workhorse of safety assessment, namely, physical testing, is no longer adequate as the sole means of ensuring safety. A standard safety assessment benchmark is to evaluate the behavior of a new design in the context of a risk-exposing test scenario. Manual or computerized analysis of the behavior of such systems is challenging because of the presence of non-linear physical dynamics, computational components, and impacts. In this paper, we study the utility of a new technology called rigorous simulation for addressing this problem. Rigorous simulation aims to combine some of the benefits of traditional simulation methods with those of traditional analytical methods such as symbolic algebra. We develop and analyze in detail a case study involving an Intersection Collision Avoidance (ICA) test scenario using the hazard analysis techniques prescribed in the ISO 26262 functional safety standard. We show that it is possible to formally model and rigorously simulate the test scenario to produce informative results about the severity of collisions. The work presented in this paper demonstrates that rigorous simulation can handle models of non-trivial complexity. The work also highlights the practical challenges encountered in using it. © 2020, Springer Nature Switzerland AG.

With the increasing level of automation in road vehicles, the traditional workhorse of safety assessment, namely, physical testing, is no longer adequate as the sole means of ensuring safety. A standard safety assessment benchmark is to evaluate the behavior of a new design in the context of a risk-exposing test scenario. Manual or computerized analysis of the behavior of such systems is challenging because of the presence of non-linear physical dynamics, computational components, and impacts. In this paper, we study the utility of a new technology called rigorous simulation for addressing this problem. Rigorous simulation aims to combine some of the benefits of traditional simulation methods with those of traditional analytical methods such as symbolic algebra. We develop and analyze in detail a case study involving an Intersection Collision Avoidance (ICA) test scenario using the hazard analysis techniques prescribed in the ISO 26262 functional safety standard. We show that it is possible to formally model and rigorously simulate the test scenario to produce informative results about the severity of collisions. The work presented in this paper demonstrates that rigorous simulation can handle models of non-trivial complexity. The work also highlights the practical challenges encountered in using it. © 2020, Springer Nature Switzerland AG.

Developing Cyber-Physical Systems requires methods and tools to support simulation and verification of hybrid (both continuous and discrete) models. The Acumen modeling and simulation language is an open source testbed for exploring the design space of what rigorous-but-practical next-generation tools can deliver to developers of Cyber-Physical Systems. Like verification tools, a design goal for Acumen is to provide rigorous results. Like simulation tools, it aims to be intuitive, practical, and scalable. However, it is far from evident whether these two goals can be achieved simultaneously.

This paper explains the primary design goals for Acumen, the core challenges that must be addressed in order to achieve these goals, the "agile research method" taken by the project, the steps taken to realize these goals, the key lessons learned, and the emerging language design. © ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2016.

Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution. ©2015 The Authors. Published by Elsevier Ltd.

Simulation traditionally computes individual trajectories, which severely limits the assessment of overall system behaviour. To address this fundamental shortcoming, we rely on computing enclosures to determine bounds on system behaviour instead of individual traces. In the present case study, we investigate the enclosures of a generic Automatic Emergency Braking (AEB) system and demonstrate how this creates a direct link between requirement specification and standardized safety criteria as put forward by ISO 26262. The case study strongly supports that a methodology based on enclosures can provide a missing link across the engineering process, from design to compliance testing. This result is highly relevant for ongoing efforts to virtualize testing and create a unified tool-chain for the development of next generation Advanced Driver Assistance Systems. © 2014, FISITA. All rights reserved.

We propose an arithmetic of function intervals as a basis for convenient rigorous numerical computation. Function intervals can be used as mathematical objects in their own right or as enclosures of functions over the reals. We present two areas of application of function interval arithmetic and associated software that implements the arithmetic: (1) Validated ordinary differential equation solving using the AERN library and within the Acumen hybrid system modeling tool. (2) Numerical theorem proving using the PolyPaver prover. © 2014 Springer-Verlag.

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs.

Even simple hybrid systems like the classic bouncing ball can exhibit Zeno behaviors. The existence of this type ofbehavior has so far forced simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad hoc restrictions to circumvent Zeno behavior or to abandon hybrid modeling. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independently of the occurrence of agiven event. Such an event can then even occur an unbounded number of times, thus making it possible to handle certain types of Zeno behavior. © 2013 IEEE.