Comparing model checkers for timed UML activity diagrams ?
Experimental study on the use of model checkers to verify properties of timed UML-Activity diagrams. Creation of a benchmark for the verification of UML-Activity diagrams. Introduction and evaluation of seven translations from UML-Activity diagrams into the input languages of four model checkers in particular: UPPAAL, PES, SPIN and NuSMV. UPPAAL achieves the best performance for timed and non-timed model, and NuSMV seems to be inadequate for the verification of UML-Activity diagrams.
uml activity diagrams uppaal spin nusmv model checking