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.