Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms

Download: PDF, ICSE 2013 slides (PDF), InvariMint implementation.

“Using declarative specification to improve the understanding, extensibility, and comparison of model-inference algorithms” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. IEEE Transactions on Software Engineering, vol. 41, no. 4, Apr. 2015, pp. 408-428.
A previous version appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. In ICSE 2013, Proceedings of the 35th International Conference on Software Engineering, (San Francisco, CA, USA), May 2013, pp. 252-261.
An extended version with proofs appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. University of Washington Department of Computer Science and Engineering technical report UW-CSE-13-03-01, (Seattle, WA, USA), Mar. 2013.
A previous version appeared as “Unifying FSM-inference algorithms through declarative specification” by Ivan Beschastnikh, Yuriy Brun, Jenny Abrahamson, Michael D. Ernst, and Arvind Krishnamurthy. University of Washington Department of Computer Science and Engineering technical report UW-CSE-12-08-02, (Seattle, WA, USA), Aug. 2012.

Abstract

It is a staple development practice to log system behavior. Numerous powerful model-inference algorithms have been proposed to aid developers in log analysis and system understanding. Unfortunately, existing algorithms are typically declared procedurally, making them difficult to understand, extend, and compare. This paper presents InvariMint, an approach to specify model-inference algorithms declaratively.

We applied the InvariMint declarative approach to two model-inference algorithms. The evaluation results illustrate that InvariMint (1) leads to new fundamental insights and better understanding of existing algorithms, (2) simplifies creation of new algorithms, including hybrids that combine or extend existing algorithms, and (3) makes it easy to compare and contrast previously published algorithms.

InvariMint's declarative approach can outperform procedural implementations. For example, on a log of 50,000 events, InvariMint's declarative implementation of the kTails algorithm completes in 12 seconds, while a procedural implementation completes in 18 minutes. We also found that InvariMint's declarative version of the Synoptic algorithm can be over 170 times faster than the procedural implementation.

Download: PDF, ICSE 2013 slides (PDF), InvariMint implementation.

BibTeX entry:

@article{BeschastnikhBAEK2015,
   author = {Ivan Beschastnikh and Yuriy Brun and Jenny Abrahamson and
	Michael D. Ernst and Arvind Krishnamurthy},
   title = {Using declarative specification to improve the understanding,
	extensibility, and comparison of model-inference algorithms},
   journal = {IEEE Transactions on Software Engineering},
   volume = {41},
   number = {4},
   pages = {408--428},
   month = apr,
   year = {2015},
   issn = {0098-5589}
}

Back to Publications that describe invariant detection techniques in Daikon.