Traditionally, debugging has been guided by heuristics and intuition, but the complexity of contemporary software, which is especially evident in the increasing number of modules and the side effects of their interactions, demands algorithmic and semiautomatic approaches.

In this paper, the authors present a two-pronged approach to debugging Java programs with infinite executions. The approach implements automated debugging by combining the abstract, model checking, with the operational, runtime monitoring. The paper presents the motivation for its approach to debugging and then provides a concrete example of a file transfer protocol (FTP) server to illustrate the techniques advanced: converting an execution trace into a sequence of states that are subject to analysis by SPIN, a model checker.

The paper formally characterizes the linear temporal logic (LTL) used to analyze the sequence of states, and details how SPIN checks properties. Following the theoretical framework for debugging, the authors discuss empirical results using FTP, network file system (NFS), and hypertext transfer protocol (HTTP) servers and the elevator problem, which models the management of competing resources.

The results demonstrate that the technique described identifies exceptions, cycles, and concurrency conditions. The paper concludes with comparisons to related work and directions for future work. Although it limits itself to Java programs, the paper provides a model for translating the techniques to other programming environments.

This paper would primarily interest systems engineers and programmers of complex, highly modularized, and interconnected software. Its strength is its attention to both abstract and operational aspects of debugging.