Efficient Large-scale Trace Checking Using MapReduce

Conference object, Preprint English OPEN
Bersani, Marcello M. ; Bianculli, Domenico ; Ghezzi, Carlo ; Krstic, Srdan ; Pietro, Pierluigi San (2015)
  • Related identifiers: doi: 10.1145/2884781.2884832
  • Subject: D.2.4 | Computer Science - Software Engineering | Computer Science - Logic in Computer Science | 68N30

The problem of checking a logged event trace against a temporal logic specification arises in many practical cases. Unfortunately, known algorithms for an expressive logic like MTL (Metric Temporal Logic) do not scale with respect to two crucial dimensions: the length of the trace and the size of the time interval for which logged events must be buffered to check satisfaction of the specification. The former issue can be addressed by distributed and parallel trace checking algorithms that can take advantage of modern cloud computing and programming frameworks like MapReduce. Still, the latter issue remains open with current state-of-the-art approaches. In this paper we address this memory scalability issue by proposing a new semantics for MTL, called lazy semantics. This semantics can evaluate temporal formulae and boolean combinations of temporal-only formulae at any arbitrary time instant. We prove that lazy semantics is more expressive than standard point-based semantics and that it can be used as a basis for a correct parametric decomposition of any MTL formula into an equivalent one with smaller, bounded time intervals. We use lazy semantics to extend our previous distributed trace checking algorithm for MTL. We evaluate the proposed algorithm in terms of memory scalability and time/memory tradeoffs.
  • References (26)
    26 references, page 1 of 3

    [1] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.

    [2] Apache Software Foundation. Hadoop MapReduce. http://hadoop.apache.org/mapreduce/.

    [3] B. Barre, M. Klein, M. Soucy-Boivin, P.-A. Ollivier, and S. Hall´e. MapReduce for parallel trace validation of LTL properties. In Proc. of RV 2012, volume 7687 of LNCS, pages 184-198. Springer, 2012.

    [4] E. Bartocci, B. Bonakdarpour, and Y. Falcone. First international competition on software for runtime verification. In Proc of RV 2014, volume 8734 of LNCS, pages 1-9. Springer, 2014.

    [5] D. Basin, G. Caronni, S. Ereth, M. Harvan, F. Klaedtke, and H. Mantel. Scalable offline monitoring. In Proc of RV 2014, volume 8734 of LNCS, pages 31-47. Springer, 2014.

    [6] D. Basin, M. Harvan, F. Klaedtke, and E. Za˘linescu. Monpoly: Monitoring usage-control policies. In Proc. of RV 2011, volume 7186 of Lecture Notes in Computer Science, pages 360-364, 2011.

    [7] D. Basin, M. Harvan, F. Klaedtke, and E. Zalinescu. Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng., 39(10):1403-1426, 2013.

    [8] A. Bauer and Y. Falcone. Decentralised LTL monitoring. In Proc of FM 2012, volume 7436 of LNCS, pages 85-100. Springer, 2012.

    [9] D. Bianculli, C. Ghezzi, and S. Krsti´c. Trace checking of metric temporal logic with aggregating modalities using MapReduce. In Proc. of SEFM 2014, volume 8702 of LNCS, pages 144-158. Springer, 2014.

    [10] D. Bianculli, C. Ghezzi, and P. San Pietro. The tale of SOLOIST: a specification language for service compositions interactions. In Proc. of FACS 2012, volume 7684, pages 55-72. Springer, 2012.

  • Metrics
    No metrics available
Share - Bookmark