Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Efficient large-scale trace checking using MapReduce
Bersani M., Bianculli D., Ghezzi C., Krstić S., San Pietro P.  ICSE 2016 (Proceedings of the 38th International Conference on Software Engineering, Austin, TX, May 14-22, 2016)888-898.2016.Type:Proceedings
Date Reviewed: Feb 13 2017

In software engineering, software verification and validation has always been a challenging task. On the other hand, the emergence of big data and cloud computing has opened a new horizon for the verification of formal software specifications in a real runtime environment. Trace checking is a traditional methodology that is normally provided with centralized and sequential running processes. In this methodology, memory saturation at the processing node can endanger its operation for high-volume information if the considered checking interval surmounts a constant or trace logs exceed a limit.

To mitigate the above-mentioned issue, a multi-faceted approach that blends metric temporal logic (MTL) with trace checking methods, for huge operational software systems, is presented. This policy has been interwoven with the MapReduce framework to fulfill its duties in a performant, distributed, and concurrent manner at a cluster of processing nodes. To implement such a capability with MTL, a new innovation, lazy semantic, is proposed. It translates the traditional MTL, point-based transactions to an equivalent with smaller, bounded time and partitioned sub-transactions, having a more illustrative nature. The sub-transactions can be mounted at different nodes and executed in a parallel and distributed environment much more reliably and quicker than the traditional and legacy ones.

A very good, attractive, and comprehensive abstract is the vanguard of the paper. It is nicely structured and organized. The authors compare the key topic of the paper, lazy semantic MTL, with point-based semantic patterns. They provide obvious and complete reasoning and related automata formulation to implement the semantics to define the time language and evaluate the timed words. Next, the joint cooperation of the lazy semantic and the MapReduce framework unveils the miracle of the lazy semantic for software verification in an operational environment. The paper finishes with an estimation of the value of the methodology with criteria like scalability and time/memory tradeoff. The paper would have been more complete if it had included a bit more information about MTL.

Reviewer:  Mohammad Sadegh Kayhani Pirdehi Review #: CR145062 (1705-0275)
Bookmark and Share
  Featured Reviewer  
Software Engineering (D.2 )
Would you recommend this review?
Other reviews under "Software Engineering": Date
Perspectives of system informatics: a comparative presentation of object-oriented programming with C++ and Java
Broy M. (ed), Zamulin A. (ed), Bjorner D., Springer-Verlag New York, Inc., Secaucus, NJ, 2002.  561, Type: Book (9783540430759)
Jul 3 2003
Relationship quality: the undervalued dimension of software quality
Russell B., Chatterjee S. Communications of the ACM 46(8): 85-89, 2003. Type: Article
Oct 14 2003
Executable JVM model for analytical reasoning: a study
Liu H., Moore J.  Interpreters, Virtual Machines and Emulators (Proceedings of the 2003 workshop, San Diego, California, Jun 12, 2003)15-23, 2003. Type: Proceedings
Sep 24 2003

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy