Automatic Generation of SPIN Model Checking Code from UML Activity Diagrams
Yutaka YAMADA, Katsumi Wasaki · International Journal of Advancements in Computing Technology · 2011
UML activity diagrams are suitable for expressing work flows and behavior at each stage of development from analysis and design to programming. This approach takes the upstream design specification of the software as a model and uses a formal language that can be verified by a model checker. We propose a method for converting UML activity diagrams automatically to the SPIN model checking code PROMELA. We modeled the screen transition design of a Web application as an evaluation of the proposed method. We were able to detect and trace counterexamples using the model checker, and found latent bugs in the design.