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 条

[41] A RAG-based Feedback Tool to Augment UML Class Diagram Learning
Ardimento, Pasquale
Bernardi, Mario Luca
Cimitile, Marta
Scalera, Michele
ACM/IEEE 27TH INTERNATIONAL CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS: COMPANION PROCEEDINGS, MODELS 2024, 2024, : 26 - 30
[42] Normalizing OCL constraints in UML class diagram-based metamodels - AND/OR clauses
Lengyel, L
Levendovszky, T
Charaf, H
Eurocon 2005: The International Conference on Computer as a Tool, Vol 1 and 2 , Proceedings, 2005, : 579 - 582
[43] Formal Verification of UML2 Timing Diagrams based on Time Petri Nets
Louati, Aymen
Barkaoui, Kamel
INTERNATIONAL JOURNAL OF INFORMATION SYSTEMS IN THE SERVICE SECTOR, 2016, 8 (02) : 87 - 97
[44] Building measure-based prediction models for UML class diagram maintainability
Genero, Marcela
Manso, Esperanza
Visaggio, Aaron
Canfora, Gerardo
Piattini, Mario
EMPIRICAL SOFTWARE ENGINEERING, 2007, 12 (05) : 517 - 549
[45] Building UML class diagram maintainability prediction models based on early metrics
Genero, M
Piattini, M
Manso, E
Cantone, G
NINTH INTERNATIONAL SOFTWARE METRICS SYMPOSIUM, PROCEEDINGS, 2003, : 263 - 275
[46] FORMAL VERIFICATION OF UML MARTE SPECIFICATIONS BASED ON A TRUE CONCURRENCY REAL TIME MODEL
Chabbat, Nadia
Saidouni, Djamel Eddine
Boukharrou, Radja
Ghanemi, Salim
COMPUTING AND INFORMATICS, 2020, 39 (05) : 1022 - 1060
[47] Formal modeling and verification of security protocols on cloud computing systems based on UML 2.3
Fang, Kunding
Li, Xiaohong
Hao, Jianye
Feng, Zhiyong
2016 IEEE TRUSTCOM/BIGDATASE/ISPA, 2016, : 852 - 859
[48] A Logic-Based Approach for the Verification of UML Timed Models
Baresi, Luciano
Morzenti, Angelo
Motta, Alfredo
Pourhashem, Mohammad Mehdi K.
Rossi, Andmatteo
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2017, 26 (02)
[49] Tightly integrate dynamic verification with formal verification: A GSTE based approach
Yang, Jin
Puder, Avi
ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 327 - 330
[50] Formal Verification of UML MARTE Specifications Based on a True Concurrency Real Time Model
Chabbat N.
Saidouni D.E.
Boukharrou R.
Ghanemi S.
Computing and Informatics, 2021, 39 (05) : 1022 - 1060

← 1 2 3 4 5 →