UML Automatic Verification Tool with Formal Methods

被引：23
|
作者：
Beato, Ma Encarnacion [1 ]
Barrio-Solorzano, Manuel [2 ]
Cuesta, Carlos E. [2 ]
de la Fuente, Pablo [2 ]
机构：
[1] Univ Salamanca, Escuela Univ Informat, Salamanca, Spain
[2] Univ Valladolid, Fac Informat, Valladolid, Spain
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 127卷 / 04期
关键词：
Formal methods; automatic verification; UML active behaviour; formal UML; verification;
D O I：
10.1016/j.entcs.2004.10.024
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The use of the UML specification language is very widespread due to some of its features. However, the ever more complex systems of today require modeling methods that allow errors to be detected in the initial phases of development. The use of formal methods make such error detection possible but the learning cost is high. This paper presents a tool which avoids this learning cost, enabling the active behavior of a system expressed in UML to be verified in a completely automatic way by means of formal method techniques. It incorporates an assistant for the verification that acts as a user guide for writing properties so that she/he needs no knowledge of either temporal logic or the form of the specification obtained.
引用
收藏
页码：3 / 16
页数：14
相关论文
共 50 条
  • [1] A Formal Verification Tool for UML Behavioral Diagrams
    Rebelo dos Santos, Luciana Brasil
    Eras, Eduardo Rohde
    de Santiago Junior, Valdivino Alexandre
    Vijaykumar, Nandamudi Lankalapalli
    [J]. COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2014, PT 1, 2014, 8579 : 696 - 711
  • [2] Automatic verification of uml state chart by bogor model checking tool Automatic formal verification of network and distributed systems
    Neysian, Behzad Soleimani
    Babamir, Seyed Morteza
    [J]. 2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 796 - 801
  • [3] Formal semantics of UML state diagram and automatic verification Based on Kripke structure
    Zhao, Yefei
    Yang Zong-yuan
    Xie, Jinkui
    [J]. 2009 IEEE 22ND CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1 AND 2, 2009, : 90 - 94
  • [4] Scalable Formal Verification of UML Models
    Kallehbasti, Mohammad Mehdi Pourhashem
    [J]. 2015 IEEE/ACM 37TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, VOL 2, 2015, : 847 - 850
  • [5] COMBINE: A Tool on Combined Formal Methods for Bindingly Verification
    Nguyen, An N.
    Quan, Tho T.
    Nguyen, Phung H.
    Bui, Thang H.
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 387 - 395
  • [6] A formal testing framework for UML statechart diagrams behaviours: From theory to automatic verification
    Latella, D
    Massink, M
    [J]. SIXTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, 2001, : 11 - 22
  • [7] Integrating UML and Formal Methods
    Borges, Rafael Magalhaes
    Mota, Alexandre Cabral
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 184 : 97 - 112
  • [8] Formal Verification of UML Statecharts using the LOTOS Formal Language
    Javani, Mohamad
    Neysiani, Behzad Soleimani
    Babamir, Seyed Morteza
    [J]. 2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 754 - 760
  • [9] Generic Methodology for Formal Verification of UML Models
    Kochaleema, K. H.
    Kumar, G. Santhosh
    [J]. DEFENCE SCIENCE JOURNAL, 2022, 72 (01) : 40 - 48
  • [10] Formal verification of UML 2.0 Sequence diagram
    Park, Sachoun
    Han, Taeman
    Kwon, Gihwon
    [J]. 22ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING & KNOWLEDGE ENGINEERING (SEKE 2010), 2010, : 411 - 416
12345