Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

Tommaso Dreossi; Alexandre Donzé; Sanjit A. Seshia

Source-linked AI summary

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia

arXiv:1703.00978v3Mar 2, 2017eess.SYcs.LGcs.SE

TL;DR

Safety-critical CPS increasingly depend on ML components whose outputs may affect system correctness, motivating systematic falsification of CPSML models. The paper proposes cooperating CPS and ML analyzers that search for STL-violating executions compositionally, and demonstrates the technique on AEBS models with deep-neural-network perception. The authors also note that scaling the approach to real autonomous-driving sensor systems remains an open practical challenge.

Problem
The paper addresses how to systematically find bugs in safety-critical CPS whose correctness depends on complex ML components and high-dimensional input spaces.
Method
The proposed framework decomposes falsification between a temporal-logic CPS Analyzer and an ML Analyzer that exchanges projected regions and searches for misclassifications leading to system-level counterexamples.
Results
The framework was implemented and shown effective on autonomous-driving AEBS controllers using perception based on multiple deep neural networks.
Takeaways & Limitations
Compositional abstraction and reasoning provide a modular way to analyze CPSML temporal properties while handling ML classifiers, including deep neural networks.
Takeaways & Limitations
Practical deployment remains limited by the high dimensionality and complexity of real autonomous-driving sensor streams and the need for substantially greater scalability.

Abstract

from arXiv · show

Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to generalize from examples, they are only as good as the examples provided, and recent efforts have shown that they can produce inconsistent output under small adversarial perturbations. This raises the question: can the output from learning components can lead to a failure of the entire CPS? In this work, we address this question by formulating it as a problem of falsifying signal temporal logic (STL) specifications for CPS with ML components. We propose a compositional falsification framework where a temporal logic falsifier and a machine learning analyzer cooperate with the aim of finding falsifying executions of the considered model. The efficacy of the proposed technique is shown on an automatic emergency braking system model with a perception component based on deep neural networks.

1 Introduction

The paper formulates CPS failures involving ML components as STL falsification and proposes a compositional framework in which CPS and ML analyzers cooperate. It demonstrates the approach on AEBS models using deep-neural-network perception.

Motivation: The paper asks how to systematically find bugs in safety-critical CPS that rely on ML components for perception and control inputs.The motivating examples include semi-autonomous vehicles with image classifiers supporting controllers for physical subsystems.
Problem formulation: CPSML falsification searches for an input that violates an STL specification and produces a counterexample trace revealing a system bug.The searched input space may include control signals and rich sensor inputs such as camera images, LiDAR, and RADAR.
Framework: The proposed compositional framework divides falsification between the ML component and the remainder of the CPS, connecting their projected search spaces.The CPS Analyzer and ML Analyzer exchange information about regions of interest or uncertainty during the search.
Framework: The ML Analyzer abstracts feature spaces, samples relevant subspaces, approximates classifiers, and identifies misclassifications that may yield system-level counterexamples.Misclassifying feature vectors are mapped back to smaller CPSML input subsets where counterexamples are easier to find.
Contributions: The framework is designed for arbitrary ML classifiers, including deep neural networks, and is presented as a modular approach to falsifying closed-loop CPS temporal properties.The authors describe it as the first approach targeting temporal-logic falsification of closed-loop CPS with ML components, including deep neural networks.
Evaluation: Experiments evaluate the approach on two AEBS instantiations using multiple deep neural networks for object detection and classification.The evaluated networks include AlexNet with Caffe, Inception-v3 with TensorFlow, and an AEBS in the Udacity self-driving car simulator.

2 Background

The background defines gray-box CPSML models, simulation traces, classifiers, and STL syntax and semantics. It also introduces quantitative robustness and validity domains used to characterize satisfaction and falsification.

CPSML Models: A gray-box CPSML model is represented as M = (S, U, sim), where the simulator maps states and inputs at discrete time steps to new states.The model includes state space S, input space U, and simulator sim, with rational positive time increments.
CPSML Models: A simulation trace records time, state, and input tuples generated by repeatedly applying the simulator over a sequence of time steps.The next state satisfies s(t_k+1) = sim(s(t_k), u(t_k), Δ_k), and t_k+1 = t_k + Δ_k.
Classifiers: The ML components are classifiers f : X → Y that assign labels to feature vectors, with false positives and false negatives counted over a test set.The error rate is based on the classifier’s false-positive and false-negative counts, while a low error rate implies good test-set predictions.
Signal Temporal Logic: STL extends linear temporal logic for CPS properties using predicates, negation, conjunction, and the until operator over time intervals.The qualitative semantics determine whether a trace satisfies a formula at a time instant, and a trace satisfies the formula when it holds at time zero.
Signal Temporal Logic: Quantitative STL semantics assign robustness values, with positive robustness equivalent to satisfaction and the robustness signal varying over time.The quantitative evaluation represents distance to satisfaction or violation.
Validity Domains: The validity domain U_ϕ contains inputs whose model traces satisfy ϕ, while U_¬ϕ contains inputs sought for falsification.The falsification challenge is difficult because the input space U can have very high dimensionality.

3 Compositional Falsification Framework

The framework decomposes CPSML falsification into analyses of an abstracted CPS and its ML components, then recombines them to search for concrete counterexamples. It targets regions where ML misclassifications may cause STL violations.

Falsification seeks an initial state and input sequence whose simulated CPSML trace violates an STL specification.
The framework separates the ML component from the remainder of the system and analyzes the two projected input spaces independently.A temporal logic falsifier analyzes the abstracted CPS, while an ML analyzer examines classifier behavior.
The ML analyzer maps misclassified feature-space inputs into a targeted CPSML input subset, after which a temporal logic falsifier searches the original model.The resulting counterexamples concern the concrete CPSML model rather than its abstractions.
Perfect and always-wrong ML abstractions define validity domains whose difference identifies a region of uncertainty where misclassifications may affect the specification.The optimistic abstraction assumes correct classifications; the pessimistic abstraction assumes misclassifications.
The approach can be truncated by treating the entire validity domain as the region of uncertainty when the pessimistic abstraction is not computed.The paper uses this truncated variant in an illustrative example and reports the full approach for the AEBS case study.

4 Machine Learning Analyzer

The ML analyzer abstracts a constrained feature space into a compact domain, approximates classifier behavior there, and searches for misclassification regions. Sampling and interpolation expose concrete image patterns associated with classifier errors.

Feature-space abstraction replaces exhaustive pixel exploration with realistic, semantically meaningful image modifications related to the system’s region of uncertainty.The motivation is to analyze images close to the training data but altered in ways relevant to system-level counterexamples.
An abstraction function maps constrained feature vectors into abstract elements, while concretization maps abstract elements back to features.These mappings connect the CPS input space with classifier feature space and enable analysis on a compact domain.
The analyzer constructs an abstract classifier by sampling concretized features, obtaining labels from the original classifier, and interpolating the sampled points.The approximation is evaluated on a test set until its error falls below a chosen threshold.
The approximation process can steer sampling toward misclassifications that may lead to system-level counterexamples and reveal clusters sharing common characteristics.These clusters support higher-level analysis of why misclassifications occur.
Low-discrepancy sampling is proposed to cover the abstract domain quickly and evenly, improving access to corner-case misclassifications.Sampling choices strongly influence approximation accuracy and insight into misclassification regions.
On 300 test cases, discrepancies between original classifiers and approximations were 0.0867 for AlexNet and 0.1733 for Inception-v3.The projections identify concrete feature-vector regions where vehicles are misclassified.
Inception-v3 correctly classified more considered road pictures than AlexNet, while AlexNet showed a pattern of correct classification when the car was near either lane.The analysis also found an isolated Inception-v3 corner-case misclassification within a cluster of correct predictions.

5 Experimental Results

Two AEBS case studies evaluate compositional falsification with ML perception components, using Simulink and Unity-Udacity models to identify misclassifications that can produce system-level counterexamples.

Case studies: The experiments cover Simulink-based and Unity-Udacity simulator-based AEBS case studies with different simulators and controllers.The first showcases abstraction-based compositional falsification; the second applies falsification directly to the concrete CPSML model while synthesizing image sequences.
Case study 1: Simulink-based AEBS: The Simulink AEBS combines vehicle-control logic, radar sensing, and a deep neural network image classifier for obstacle detection.The classifier alerts the AEBS for obstacles beyond the radar’s 30m range, while the controller transitions among safe, warning, braking, and collision-mitigation modes.
Case study 1: Simulink-based AEBS: Figure 7 compares validity domains under correct classification and optimistic or pessimistic ML abstractions, highlighting a region of uncertainty where misclassification may affect the property.Initial velocity and distance form the axes; green denotes satisfaction and red denotes falsification.
Case study 1: Simulink-based AEBS: The STL property G(¬(dist(t)) ≤0) requires the vehicle-obstacle distance to remain positive, with initial velocity in [0, 40] mph and distance in [0, 60] m.The preceding vehicle is stationary, and the input space also includes all RGB images of size 1000 × 600.
Case study 1: Simulink-based AEBS: The ML analyzer maps candidate CPS counterexamples into abstract image features, enabling targeted searches for misclassified pictures that may violate the STL property.One candidate is (25, 40), representing an initial velocity of 25 and distance of 40.
Case study 1: Simulink-based AEBS: Changing only the abstract feature’s x position changed robustness from −24.38 to 12.41 for input (31, 56), converting a falsifying input into a non-falsifying one.For another input, (27, 45), robustness changed from falsifying to 9.09 after the x-position alteration.
Case study 1: Simulink-based AEBS: Inception-v3’s tested corner-case misclassification did not change the computed falsification points, indicating that this misclassification might not affect CPSML correctness.The corresponding distance was 4.88, with falsification points at velocities from 4 to 40 mph.
Case study 2: Unity-Udacity simulator-based AEBS: In the Unity-Udacity case study, simulations using misclassifying images identified by the analysis mostly caused the car to collide with the cow.The CNN classified onboard-camera images as “cow” or “not cow,” and the AEBS controlled acceleration and braking.

6 Conclusion

The paper presents a compositional falsification framework for CPSML models and outlines extensions toward improved ML analysis, interpretable training-data insights, verification, and broader applications.

The framework decomposes CPSML falsification into system and machine-learning analysis, using abstracted feature spaces and misclassified vectors to drive the search.The ML analyzer abstracts feature spaces, approximates classifiers, and provides misclassified feature-vector sets for falsification.
Improvements in the ML Analyzer: The ML Analyzer is intended to generate feature-space abstractions automatically from training sets and exploit the structure of specialized ML architectures.The authors mention sensitivity analysis as one possible way to identify directions in abstract space that change classifier outputs.
Impacting the ML component design: The approach can produce higher-level insight into training-data gaps, additional scenarios for training, and learning-algorithm parameter adjustments.This extends the usefulness of falsification beyond individual violating input sequences toward ML-component design.
From Falsification to Verification: The compositional framework could support CPSML verification when abstract-system safety can be proved and a refinement strategy covers the region of uncertainty.The paper identifies this as future work rather than a completed verification result.
Further Applications: Practical deployment remains constrained by high-dimensional, multimodal sensor streams and the need to scale analysis substantially for industrial autonomous-driving systems.The paper identifies cameras, LIDAR, RADAR, sensor fusion, video streams, and possible cloud infrastructure as relevant scaling challenges.