Formal specification methods (FSMs) have not been widely accepted in the software industry. The problems with FSMs are discussed. Most important are the communication problem with the customer when using FSMs; that software developers lack formal training in applying FSMs; that most research in FSMs concentrates on formal notation and inference rules, instead of offering a methodology for their use; and a lack of experience with FSMs in large-scale applications.

Next, the authors present a sketch of formal specification and an overview of FSMs. The main purpose of the paper, however, is to classify FSMs using a framework. The dimensions used are whether formalization is direct or transitional, and whether it is unassisted or computer assisted. The transitional approach is subdivided into sequential and parallel successive refinement.

The resulting taxonomy is quite interesting. Five of the six regions contain example FSMs, but no FSM has been reported that can be classified as a computer-assisted (transitional) parallel refinement method.

An important conclusion of the paper is that “transitional computer-assisted strategies provide most promise in addressing the scalability problem.”

This paper is suitable for a wide audience, but is of particular interest to researchers in FSMs and industrial software developers.