Tommaso Dreossi and Alexandre Donze and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2017-165

November 26, 2017

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-165.pdf

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

---

BibTeX citation:

@techreport{Dreossi:EECS-2017-165,
    Author= {Dreossi, Tommaso and Donze, Alexandre and Seshia, Sanjit A.},
    Title= {Compositional Falsification of Cyber-Physical Systems with Machine Learning Components},
    Year= {2017},
    Month= {Nov},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-165.html},
    Number= {UCB/EECS-2017-165},
    Abstract= {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
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.},
}

EndNote citation:

%0 Report
%A Dreossi, Tommaso 
%A Donze, Alexandre 
%A Seshia, Sanjit A. 
%T Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
%I EECS Department, University of California, Berkeley
%D 2017
%8 November 26
%@ UCB/EECS-2017-165
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2017/EECS-2017-165.html
%F Dreossi:EECS-2017-165