Simulation-based Adversarial Test Generation for Autonomous Vehicles with Machine Learning Components, (arxiv)
Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, James Kapinski, (IV 2018)
Many organizations are developing autonomous driving systems, which are expected to be deployed at a large scale in the near future. Despite this, there is a lack of agreement on appropriate meth- ods to test, debug, and certify the performance of these systems. One of the main challenges is that many autonomous driving systems have machine learning components, such as deep neural net- works, for which formal properties are difficult to characterize. We present a testing framework that is compatible with test case generation and automatic falsification methods, which are used to evalu- ate cyber-physical systems. We demonstrate how the framework can be used to evaluate closed-loop properties of an autonomous driving system model that includes the ML components, all within a vir- tual environment. We demonstrate how to use test case generation methods, such as covering arrays, as well as requirement falsification methods to automatically identify problematic test scenarios. The resulting framework can be used to increase the reliability of autonomous driving systems.
Reasoning about Safety of Learning-Enabled Components in Autonomous Cyber-physical Systems, (arxiv)
Cumhur Erkan Tuncali, James Kapinski, Hisahiro Ito, Jyotirmoy V. Deshmukh, (DAC 2018)
We present a simulation-based approach for generating barrier certificate functions for safety verification of cyber-physical systems (CPS) that contain neural network-based controllers. A linear programming solver is utilized to find a candidate generator function from a set of simulation traces obtained by randomly selecting initial states for the CPS model. A level set of the generator function is then selected to act as a barrier certificate for the system, meaning it demonstrates that no unsafe system states are reachable from a given set of initial states. The barrier certificate properties are verified with an SMT solver. This approach is demonstrated on a case study in which a Dubins car model of an autonomous vehicle is controlled by a neural network to follow a given path.
Poster: Sim-ATAV: Simulation-Based Adversarial Testing Framework for Autonomous Vehicles, (acm)
Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, James Kapinski, (HSCC 2018)
(Best Poster Finalist)
One of the main challenges in testing autonomous driving systems is the presence of machine learning components, such as neural networks, for which formal properties are difficult to establish. We present a simulation-based testing framework that supports methods used to evaluate cyber-physical systems, such as test case generation and automatic falsification. We demonstrate how the framework can be used to evaluate closed-loop properties of autonomous driving system models that include machine learning components.
Experience Report: Application of Falsification Methods on the UxAS System, (pdf)
Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos, Sriram Sankaranarayanan, (NFM 2018)
In this report, we present our experiences in applying falsification methods over the Unmanned Systems Autonomy Services (UxAS) system. UxAS is a collection of software modules that enables complex mission planning for multiple vehicles. To test the system, we utilized the tool S-TaLiRo to generate mission scenarios for both UxAS and the underlying vehicle simulators, with the goal of finding behaviors which do not meet system specifications.
Functional Gradient Descent Optimization for Automatic Test Case Generation for Vehicle Controllers, (pdf)
Cumhur Erkan Tuncali, Shakiba Yaghoubi, Theodore Pavlic, Georgios Fainekos, (CASE 2017)
A hierarchical framework is proposed for improving the automatic test case generation process for high-fidelity models with long execution times. The framework incorporates related low-fidelity models for which certain properties can be analytically or computationally evaluated with provable guarantees (e.g., gradients of safety or performance metrics). The low-fidelity models drive the test case generation process for the high-fidelity models. The proposed framework is demonstrated on a model of a vehicle with Full Range Adaptive Cruise Control with Collision Avoidance (FRACC), for which it generates more challenging test cases on average compared to test cases generated using Simulated Annealing.
Utilizing S-TaLiRo As an Automatic Test Generation Framework for Autonomous Vehicles, (pdf)
Cumhur Erkan Tuncali, Theodore Pavlic, Georgios Fainekos, (ITSC 2016)
This paper proposes an approach to automatically generating test cases for testing motion controllers of autonomous vehicular systems. Test scenarios may consist of single or multiple vehicles under test at the same time. Tests are performed in simulation environments. The approach is based on using a robustness metric for evaluating simulation outcomes as a cost function. Initial states and inputs are updated by stochastic optimization methods between the tests for achieving smaller robustness values. The test generation framework has been implemented in the toolbox S-TaLiRo. The proposed framework's ability to generate interesting test cases is demonstrated by a case study.
Automatic Parallelization of Simulink Models on Multi-core Architectures, (pdf,
Cumhur Erkan Tuncali, Georgios Fainekos, Yann-Hang Lee, (ICESS 2015)
This paper addresses the problem of parallelizing existing single-rate Simulink models for embedded control applications on multi-core architectures considering communication cost between blocks on different CPU cores. Utilizing the block diagram of the Simulink model, we derive the dependency graph between the different blocks. In order to solve the scheduling problem, we describe a Mixed Integer Linear Programming (MILP) formulation for optimally mapping the Simulink blocks to different CPU cores. Since the number of variables and constraints for MILP solver grows exponentially when model size increases, solving this problem in a reasonable time becomes harder. For addressing this issue, we introduce a set of techniques for reducing the number of constraints in the MILP formulation. By using the proposed techniques, the MILP solver finds solutions that are closer to the optimal solution within a given time bound. We study the scalability and efficiency of our consisting approach with synthetic benchmarks of randomly generated directed acyclic graphs. We also use the "Fault-Tolerant Fuel Control System" demo from Simulink and a Diesel engine controller from Toyota as case studies for demonstrating applicability of our approach to real world problems.
Modeling Concurrency and Reconfiguration in Vehicular Systems: A pi-calculus Approach (pdf,
Joseph Campbell, Cumhur Erkan Tuncali, Theodore Pavlic, Georgios Fainekos, (ITSC 2016)
As autonomous or semi-autonomous vehicles are deployed on the roads, they will have to eventually start communicating with each other in order to achieve increased efficiency and safety. Current approaches in the control of collaborative vehicles primarily consider homogeneous simplified vehicle dynamics and usually ignore any communication issues. This raises an important question of how systems without the aforementioned limiting assumptions can be modeled, analyzed and certified for safe operation by both industry and governmental agencies. In this work, we propose a modeling framework where communication and system reconfiguration is modeled through $\pi$-calculus expressions while the closed-loop control systems are modeled through hybrid automata. We demonstrate how the framework can be utilized for modeling and simulation of platooning behaviors of heterogeneous vehicles.