This paper discusses the experimental results of a test of the verification environment, called HD-Automata Laboratory (HAL), for the finite-state verification of systems specified in the Pi-calculus. More specifically, HAL exploits history-dependent automata (HD-automata), and components that support verification by model checking of properties specified as temporal logic. The applicability of the HAL is shown by a few case studies.

The main contributions of this paper are its use of Pi-calculus as an appropriate abstraction to specify complex (global) computing systems, a faithful mapping and reduction technique that translates Pi-calculus representations to the more manageable finite state machines, and use of existing model-checking facilities to reason about the properties of a system represented in temporal logic formula.

The paper is well written and well organized. However, the key feature of this paper is its discussion of the verification of the properties of a global computing system, specified in temporal logic using model checking and finite-state automata. In case of omissions and errors in the initial specification (for example, Pi-calculus), the model checker will generate a counterexample as a hint to users. Tracing back a counterexample, which will be represented in finite-state, to Pi-calculus requires another faithful translation. The process of re-mapping and/or re-interpreting the specification by users can be error-prone and counterproductive.