Compositional Verification without Compositional Specification for Learning-Based Systems

Sanjit A. Seshia. Compositional Verification without Compositional Specification for Learning-Based Systems. Technical Report UCB/EECS-2017-164, EECS Department, University of California, Berkeley, 2017.

Download

[HTML] 

Abstract

We consider the problem of performing compositional verification of a system with machine learning components whose behavior cannot easily be formally specified. We present an approach involving a system-level verifier communicating with a component-level analyzer wherein the former identifies a subset of environment behaviors that might lead to a system-level failure while the latter identifies erroneous behaviors, such as misclassifications, of the machine learning component that might be extended to a system-level counterexample. Results on cyber-physical systems with deep learning components used for perception demonstrate the promise of this approach.

BibTeX

@techreport{seshia-tr17,
    Author = {Seshia, Sanjit A.},
    Title = {Compositional Verification without Compositional Specification for Learning-Based Systems},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2017},
    Month = {Nov},
    number = {UCB/EECS-2017-164},
    abstract = {We consider the problem of performing compositional verification 
of a system with machine learning components whose behavior 
cannot easily be formally specified.  
We present an approach involving a system-level verifier 
communicating with a component-level analyzer wherein  
the former identifies a subset of environment behaviors 
that might lead to a system-level failure while the latter 
identifies erroneous behaviors, such as misclassifications, 
of the machine learning component that might be extended 
to a system-level counterexample. 
Results on cyber-physical systems with deep learning 
components used for perception demonstrate the promise of 
this approach.}
}