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