Comparing model checkers for timed UML activity diagrams

被引:9
|
作者
Daw, Zamira [1 ]
Cleaveland, Rance [1 ]
机构
[1] Univ Maryland, Dept Comp Sci, College Pk, MD 20742 USA
基金
美国国家科学基金会;
关键词
Model checking; UML activity diagrams; UPPAAL; SPIN; NuSMV;
D O I
10.1016/j.scico.2015.05.008
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:277 / 299
页数:23
相关论文
共 50 条
  • [31] Supporting UML activity diagrams using organizational models
    Bhuiyan, Moshiur
    Islam, M. M. Zahidul
    Koliadis, George
    Krishna, Aneesh
    Ghose, Aditya
    CHALLENGES IN INFORMATION TECHNOLOGY MANAGEMENT, 2008, : 182 - 188
  • [32] Removal of Redundant Elements within UML Activity Diagrams
    Beckmann, Martin
    Michalke, Vanessa N.
    Vogelsang, Andreas
    Schlutter, Aaron
    2017 ACM/IEEE 20TH INTERNATIONAL CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS (MODELS 2017), 2017, : 334 - 343
  • [33] Making UML activity diagrams object-oriented
    Kleppe, A
    Warmer, J
    TECHNOLOGY OF OBJECT-ORIENTED LANGUAGES - TOOLS 33, PROCEEDINGS, 2000, : 288 - 299
  • [34] On the Computational Complexity of the Reachability Problem in UML Activity Diagrams
    Tan, Xing
    Gruninger, Michael
    2009 IEEE INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTING AND INTELLIGENT SYSTEMS, PROCEEDINGS, VOL 2, 2009, : 572 - 576
  • [35] Automatic translation UML activity diagrams to Petri net
    Vladimiriovich, Markov Alexandr
    Alexandrovich, Voevoda Alexandr
    Olegovich, Romannikov Dmitry
    2015 INTERNATIONAL SIBERIAN CONFERENCE ON CONTROL AND COMMUNICATIONS (SIBCON), 2015,
  • [36] Model and Criteria for the Automated Refactoring of the UML Class Diagrams
    Nikulchev, Evgeny
    Deryugina, Olga
    INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND APPLICATIONS, 2016, 7 (12) : 76 - 79
  • [37] Extending UML sequence diagrams to model agent mobility
    Kusek, Mario
    Jezic, Gordan
    AGENT-ORIENTED SOFTWARE ENGINEERING VII, 2007, 4405 : 51 - +
  • [38] A comparison of model transformation tools: Application for Transforming GRAI Extended Actigrams into UML Activity Diagrams
    Ben Salem, Ramzi
    Grangel, Reyes
    Bourey, Jean-Pierre
    COMPUTERS IN INDUSTRY, 2008, 59 (07) : 682 - 693
  • [39] Transforming GRAI extended actigrams into UML activity diagrams: a first step to model driven interoperability
    Grangel, Reyes
    Ben Salem, Ramzi
    Bourey, Jean-Pierre
    Daclin, Nicolas
    Ducq, Yves
    ENTERPRISE INTEROPERABILITY II: NEW CHALLENGES AND APPROACHES, 2007, : 447 - 458
  • [40] A Meta-Model Transformation from UML Activity Diagrams to Event-B Models
    Ben Younes, Ahlem
    Hlaoui, Yousra Bendaly
    Ben Ayed, Leila Jemni
    2014 38TH ANNUAL IEEE INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSACW 2014), 2014, : 740 - 745