Abstract. A new method for analysis and verification of Use Case Maps (UCM) specifications with the help of colored Petri nets and SPIN model checker is presented. Standardized UCM notation is a convenient visual language that allows formal expression of functional requirements. Algorithms for translation of UCM-specifications into colored Petri nets and colored Petri nets into input language Promela of the SPIN model checker are described. The complexity of the derived colored Petri nets is evaluated. We demonstrate the application of the translation algorithms and developed toolset in a case study. A simple network protocol is corrected and verified after several errors have been found in the source UCM-specification.

Keywords: verification, specification, distributed system, Use Case Map notation, colored Petri net, SPIN model checker.