VERIFYING UCM SPECIFICATIONS OF DISTRIBUTED SYSTEMS USING COLORED PETRI NETS

摘要

This article presents a new method for the analysis and verification of Use Case Map (UCM) specifications with the help of colored Petri nets and the SPIN model checker. Standardized UCM notation is a convenient visual language that allows one to formally represent functional requirements. Algorithms for translating UCM specifications into colored Petri nets and colored Petri nets into the input language Promela of the SPIN model checker are described. The complexity of the obtained colored Petri nets is evaluated. The execution of the presented translation algorithms and support tools is illustrated by the example of error localization and correction in the initial UCM specification of a simple network protocol.