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 条
  • [21] On the role of activity diagrams in UML - A user task centered development process for UML
    Paech, B
    UNIFIED MODELING LANGUAGE: UML'98: BEYOND THE NOTATION, 1999, 1618 : 267 - 277
  • [22] Model-based testing using UML activity diagrams: A systematic mapping study
    Ahmad, Tanwir
    Iqbal, Junaid
    Ashraf, Adnan
    Truscan, Dragos
    Porres, Ivan
    COMPUTER SCIENCE REVIEW, 2019, 33 : 98 - 112
  • [23] Comprehensibility of system models during test design: a controlled experiment comparing UML activity diagrams and state machines
    Michael Felderer
    Andrea Herrmann
    Software Quality Journal, 2019, 27 : 125 - 147
  • [24] Synthesis of test scenarios using UML activity diagrams
    Ashalatha Nayak
    Debasis Samanta
    Software & Systems Modeling, 2011, 10 : 63 - 89
  • [25] Synthesis of test scenarios using UML activity diagrams
    Nayak, Ashalatha
    Samanta, Debasis
    SOFTWARE AND SYSTEMS MODELING, 2011, 10 (01): : 63 - 89
  • [26] ON π-CALCULUS SEMANTICS AS A FORMAL BASIS FOR UML ACTIVITY DIAGRAMS
    Lam, Vitus W.
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2008, 18 (04) : 541 - 567
  • [27] UML Activity Diagrams in Requirements Specification of Logic Controllers
    Grobelna, Iwona
    Grobelny, Michal
    INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2015 (ICCMSE 2015), 2015, 1702
  • [28] Comprehensibility of system models during test design: a controlled experiment comparing UML activity diagrams and state machines
    Felderer, Michael
    Herrmann, Andrea
    SOFTWARE QUALITY JOURNAL, 2019, 27 (01) : 125 - 147
  • [29] Automated Scenario Generation based on UML Activity Diagrams
    Sapna, P. G.
    Mohanty, Hrushikesha
    ICIT 2008: PROCEEDINGS OF THE 11TH INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY, 2008, : 209 - 214
  • [30] Test cases generation from UML activity diagrams
    Kim, Hyungchoul
    Kang, Sungwon
    Baik, Jongmoon
    Ko, Inyoung
    SNPD 2007: EIGHTH ACIS INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, ARTIFICIAL INTELLIGENCE, NETWORKING, AND PARALLEL/DISTRIBUTED COMPUTING, VOL 3, PROCEEDINGS, 2007, : 556 - +