Walters discusses the specification of a system in a graphical modeling notation known as RDT, and the translation of RDT into Promela code (the input to the SPIN model checker). To validate the approach, a very simple example is used. The main contribution of this paper is the specification of a very trivial system in RDT, and the mapping process by which RDT will be converted to the Promela code.

The paper is relatively challenging to read, because of errors in the figures. The case study used in the paper is too simple to show the important features (for example, concurrency) of a nontrivial system. The discussion of the mapping process from RDT to Promela is incomplete and superficial. The main justification for converting from RDT to Promela and SPIN is to use the analyzing capabilities offered by SPIN. The author did not show this. More specifically, the author did not show how SPIN could be used to analyze a complete system, or how the feedback from SPIN could be used to detect a problem and correct a system originally modeled in RDT (namely, going from the bottom, SPIN, to the top, RDT).