Comparing model checkers for timed 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. (C) 2015 Elsevier B.V. All rights reserved.