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 subtraces, with a particular focus on digital circuits. We propose a novel sparse coding method that extracts specifications in the form of basis subtraces. For a set of finite subtraces each of length p, each subtrace is decomposed into a sparse Boolean combination of only a small number of basis subtraces of the same dimension. We formally define this decomposition as the 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alexe, G., Alexe, S., Crama, Y., Foldes, S., Hammer, P.L., Simeone, B.: Consensus algorithms for the generation of all maximal bicliques. Discrete Appl. Math. 145, 11–21 (2004)
Ammons, G., BodÃk, R., Larus, J.R.: Mining specifications. In: POPL, pp. 4–16 (2002)
Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97–105 (2003)
Buechi, J.R.: On a Decision Method in Restricted Second-Order Arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford University Press (1962)
de Paula, F.M., Gort, M., Hu, A.J., Wilton, S.J.E., Yang, J.: Backspace: Formal analysis for post-silicon debug. In: FMCAD, pp. 1–10 (2008)
Dodoo, N., Lin, L., Ernst, M.D.: Selecting, refining, and evaluating predicates for program analysis. Technical Report MIT-LCS-TR-914, MIT Laboratory for Computer Science (2003)
Engler, D., et al.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: SOSP, pp. 57–72 (2001)
Ernst, M., et al.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35–45 (2007)
Froidure, V.: Rangs des relations binaires, semigrollpes de relations non ambigues. PhD thesis (June 1995)
Gabel, M., Su, Z.: Javert: fully automatic mining of general temporal properties from dynamic traces. In: FSE, pp. 339–349 (2008)
Gaspers, S., Kratsch, D., Liedloff, M.: On Independent Sets and Bicliques in Graphs. In: Broersma, H., Erlebach, T., Friedetzky, T., Paulusma, D. (eds.) WG 2008. LNCS, vol. 5344, pp. 171–182. Springer, Heidelberg (2008)
Gold, E.M.: Complexity of automatic identification from given data 37, 302–320 (1978)
Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. Software Tools for Technology Transfer (STTT) 8(3), 229–247 (2006)
Harrold, M.J., Rothermel, G., Sayre, K., Wu, R., Yi, L.: An empirical investigation of the relationship between spectra differences and regression faults. Softw. Test., Verif. Reliab. 10(3), 171–194 (2000)
Lee, H., Battle, A., Raina, R., Ng, A.Y.: Efficient sparse coding algorithms. In: NIPS, pp. 801–808 (2007)
Li, W., Forin, A., Seshia, S.A.: Scalable specification mining for verification and diagnosis. In: Design Automation Conference (DAC), pp. 755–760 (June 2010)
Liblit, B., Aiken, A., Zheng, A.X., Jordan, M.I.: Bug isolation via remote program sampling. In: PLDI, pp. 141–154 (2003)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc., New York (1992)
Miettinen, P.: Sparse boolean matrix factorizations. In: Proceedings of the 2010 IEEE International Conference on Data Mining, ICDM 2010, pp. 935–940. IEEE Computer Society, Washington, DC (2010)
Miettinen, P., Mielikäinen, T., Gionis, A., Das, G., Mannila, H.: The Discrete Basis Problem. In: Fürnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) PKDD 2006. LNCS (LNAI), vol. 4213, pp. 335–346. Springer, Heidelberg (2006)
Mitra, S., Seshia, S.A., Nicolici, N.: Post-silicon validation: Opportunities, challenges and recent advances. In: Proceedings of the Design Automation Conference (DAC), pp. 12–17 (June 2010)
Park, S.B., Bracy, A., Wang, H., Mitra, S.: Blog: Post-silicon bug localization in processors using bug localization graphs. In: DAC (2010)
Peeters, R.: The maximum edge biclique problem is NP-complete. Discrete Applied Mathematics 131(3), 651–654 (2003)
Siewert, D.J.: Biclique covers and partitions of bipartite graphs and digraphs and related matrix ranks of 0,1 matrices. PhD thesis (2000)
Tasiran, S., Keutzer, K.: Coverage metrics for functional validation of hardware designs. IEEE Design & Test of Computers 18(4), 36–45 (2001)
Vaidya, J., Atluri, V., Guo, Q.: The role mining problem: Finding a minimal descriptive set of roles. In: Symposium on Access Control Models and Technologies (SACMAT), pp. 175–184 (2007)
Weimer, W., Necula, G.C.: Mining Temporal Specifications for Error Detection. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 461–476. Springer, Heidelberg (2005)
Yang, J., et al.: Perracotta: mining temporal api rules from imperfect traces. In: ICSE, pp. 282–291 (2006)
Zhu, C.S., Weissenbacher, G., Malik, S.: Post-silicon fault localisation using maximum satisfiability and backbones. In: FMCAD (2011)
Zou, H., Hastie, T., Tibshirani, R.: Sparse principal component analysis. Journal of Computational and Graphical Statistics 15, 2006 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Li, W., Seshia, S.A. (2013). Sparse Coding for Specification Mining and Error Localization. In: Qadeer, S., Tasiran, S. (eds) Runtime Verification. RV 2012. Lecture Notes in Computer Science, vol 7687. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35632-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-35632-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35631-5
Online ISBN: 978-3-642-35632-2
eBook Packages: Computer ScienceComputer Science (R0)