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.

This paper describes the results of an experimental study on the use of model checkers to verify properties of UML activity diagrams. The motivation for the study derives from the desirability of checking properties of systems early in the development process, and the fact that UML is a commonly used notation for system models. The study assesses the performance of different model checking tools, and strategies for converting activity diagrams into the tools input notation, for a class of real time activity diagrams used in medical device design. This paper compares different translations for four model checkers in particular: UPPAAL, PES, SPIN and NuSMV. The performance of these model checkers is then compared using a suite of UML activity diagrams of varying complexity developed by us for this purpose. The results of a case study involving the design of an infusion pump are also presented.