UCVSC: A Formal Approach to UML Class Diagram Online Verification Based on Situation Calculus

被引：0
|
作者：
Tan, Li [1 ]
Yang, Zongyuan [1 ]
Xie, Jinkui [1 ]
机构：
[1] E China Normal Univ, Dept Comp Sci & Technol, Shanghai 200062, Peoples R China
来源：
ICCIT: 2009 FOURTH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCES AND CONVERGENCE INFORMATION TECHNOLOGY, VOLS 1 AND 2 | 2009年
关键词：
UCVSC; UML class diagram; XMI; situation calculus; online prototype system;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The gap between informal models used in a UML environment and formal verifications and proofs in academic research prevents UML from valid and efficient application. In this paper, we propose an approach to bridge the gap between UML class diagram and situation calculus via our formal verification tool, UCVSC (UML Class diagram online Verification based on Situation Calculus). UML class diagram describes a software system informally while situation calculus is employed as the underlying formalism to precisely specify the system. With respect to most components in UML class diagram, the strength of reasoning about actions and describing the state of the world in situation calculus can be applied to represent them appropriately. Using UML tools and predefined mapping mechanism, we transform UML class diagram to XMI, an intermediate format, and finally to situation calculus in Prolog syntax. This approach attempts to provide precise semantics of UML class diagram which can be logically verified. In addition, we automate the verification process in an online prototype system. Furthermore, a case study on an academic system is presented to illustrate and evaluate our approach.*
引用
收藏
页码：375 / 380
页数：6
相关论文
共 50 条
  • [1] Formal verification of UML 2.0 Sequence diagram
    Park, Sachoun
    Han, Taeman
    Kwon, Gihwon
    22ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING & KNOWLEDGE ENGINEERING (SEKE 2010), 2010, : 411 - 416
  • [2] Formal semantics of UML state diagram and automatic verification Based on Kripke structure
    Zhao, Yefei
    Yang Zong-yuan
    Xie, Jinkui
    2009 IEEE 22ND CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1 AND 2, 2009, : 90 - 94
  • [3] Formal semantics and reasoning about UML class diagram
    Szlenk, Marcin
    DEPCOS-RELCOMEX 2006, 2006, : 51 - 58
  • [4] Formal Sequence: Extending UML Sequence Diagram for Behavior Description and Formal Verification
    Han, Deshuai
    Xing, Jianchun
    Yang, Qiliang
    Wang, Hongda
    Zhang, Xuewei
    PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2, 2016, : 474 - 481
  • [5] Taming the frame problem: an automated approach for robust UML class diagram specification and verification
    Viesca, Antonio Rosales
    Al Lail, Mustafa
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2024, : 619 - 641
  • [6] Formal Specification and Verification of Few Combined Fragments of UML Sequence Diagram
    Zafar, Nazir Ahmad
    ARABIAN JOURNAL FOR SCIENCE AND ENGINEERING, 2016, 41 (08) : 2975 - 2986
  • [7] Formal Specification and Verification of Few Combined Fragments of UML Sequence Diagram
    Nazir Ahmad Zafar
    Arabian Journal for Science and Engineering, 2016, 41 : 2975 - 2986
  • [8] Automated Mitigation of Frame Problem in UML Class Diagram Verification
    Viesca, Antonio Rosales
    Al Lail, Mustafa
    2023 ACM/IEEE INTERNATIONAL CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS COMPANION, MODELS-C, 2023, : 841 - 850
  • [9] Redesign of UML class diagrams: a formal approach
    Piotr Kosiuczenko
    Software & Systems Modeling, 2009, 8 : 165 - 183
  • [10] Redesign of UML class diagrams: a formal approach
    Kosiuczenko, Piotr
    SOFTWARE AND SYSTEMS MODELING, 2009, 8 (02): : 165 - 183
12345