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 条
  • [21] Parallel Verification of UML Using DiVinE Tool
    Basit-Ur-Rahim, Muhammad Abdul
    Ahmad, Jamil
    Arif, Fahim
    [J]. 2013 5TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY (CSIT), 2013, : 49 - 53
  • [22] AnimUML as a UML Modeling and Verification Teaching Tool
    Jouault, Frederic
    Sebille, Valentin
    Besnard, Valentin
    Le Calvar, Theo
    Teodorov, Ciprian
    Brun, Matthias
    Delatour, Jerome
    [J]. 24TH ACM/IEEE INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING LANGUAGES AND SYSTEMS COMPANION (MODELS-C 2021), 2021, : 616 - 620
  • [23] Tool Support for Consistency Verification of UML Diagrams
    Phuklang, Salilthip
    Yokogawa, Tomoyuki
    Leelaprute, Pattara
    Arimoto, Kazutami
    [J]. PRODUCT-FOCUSED SOFTWARE PROCESS IMPROVEMENT (PROFES 2017), 2017, 10611 : 606 - 609
  • [24] Formal Verification of UML Sequence Diagrams in the Embedded Systems Context
    Cunha, E.
    Custodio, M.
    Rocha, H.
    Barreto, R.
    [J]. 2011 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEM ENGINEERING (SBESC), 2011, : 39 - 45
  • [25] Formal modeling and verification of UML Activity Diagrams (UAD) with FoCaLiZe
    Abbas, Messaoud
    Rioboo, Renaud
    Ben-Yelles, Choukri-Bey
    Snook, Colin F.
    [J]. JOURNAL OF SYSTEMS ARCHITECTURE, 2021, 114
  • [26] UML to B: Formal verification of object-oriented models
    Lano, K
    Clark, D
    Androutsopoulos, K
    [J]. INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 : 187 - 206
  • [27] Formal modeling and verification of UML Activity Diagrams (UAD) with FoCaLiZe
    Abbas, Messaoud
    Rioboo, Renaud
    Ben-Yelles, Choukri-Bey
    Snook, Colin F.
    [J]. Journal of Systems Architecture, 2021, 114
  • [28] Formal verification of UML statecharts with real-time extensions
    David, A
    Möller, MO
    Yi, W
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2306 : 218 - 232
  • [29] Towards formal verification of UML diagrams based on graph transformation
    Zhao, Y
    Fan, YS
    Bai, XM
    Wang, Y
    Cai, H
    Ding, W
    [J]. PROCEEDINGS OF THE IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY FOR DYNAMIC E-BUSINESS, 2004, : 180 - 187
  • [30] Formal verification of secure group communication protocols modelled in UML
    de Saqui-Sannes, P.
    Villemur, T.
    Fontan, B.
    Mota, S.
    Bouassida, M. S.
    Chridi, N.
    Chrisment, I.
    Vigneron, L.
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 125 - 133
12345