Sparse Coding for Specification Mining and Error Localization

Wenchao Li and Sanjit A. Seshia. Sparse Coding for Specification Mining and Error Localization. In Proceedings of the International Conference on Runtime Verification (RV), September 2012.

Download

[pdf] 

Abstract

Formal specifications play a central role in the design, verification, and debugging of systems. This paper presents a new viewpoint to the problem of mining specifications from simulation or execution traces of reactive systems. The main application of interest is to localize faults to sections of an error trace we term <i>subtraces</i>, with a particular focus on digital circuits. We propose a novel sparse coding method that extracts specifications in the form of <i>basis subtraces</i>. For a set of finite subtraces each of length $p$, each subtrace is decomposed into a <i>sparse</i> Boolean combination of only a small number of basis subtraces of the same dimension. We formally define this decomposition as the <i>sparse Boolean matrix factorization problem</i> and give a graph-theoretic algorithm to solve it. We formalize a sufficient condition under which our approach is sound for error localization. Additionally, we give experimental results demonstrating that (1) we can mine useful specifications using our sparse coding method, and (2) the computed bases can be used to do simultaneous error localization and error explanation.

BibTeX

@InProceedings{li-rv12,
    Author = {Wenchao Li and Sanjit A. Seshia},
    Title = {Sparse Coding for Specification Mining and Error Localization},
    booktitle = {Proceedings of the International Conference on Runtime Verification (RV)},
    Year = {2012},
    Month = {September},
    Abstract = {Formal specifications play a central role in the design, verification, and debugging of systems.  
This paper presents a new viewpoint to the problem of mining specifications 
from simulation or execution traces of reactive systems. 
The main application of interest is to localize faults to sections of 
an error trace we term {\em subtraces}, with a particular focus on digital circuits. 
We propose a novel sparse coding method that extracts specifications in the form of {\em basis subtraces}. 
For a set of finite subtraces each of length $p$, each subtrace is decomposed 
into a {\em sparse} Boolean combination 
of only a small number of basis subtraces of the same dimension. 
We formally define this decomposition as the {\em sparse Boolean matrix factorization problem} 
and give a graph-theoretic algorithm to solve it.  
We formalize a sufficient condition under which our approach is sound for error localization. 
Additionally, we give experimental results demonstrating that 
(1) we can mine useful specifications using our sparse coding method, and (2) the computed bases can be used to do  
simultaneous error localization and error explanation.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Tue Sep 04, 2012 23:44:26