On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation using Isabelle/HOL

被引：11
作者：
Meghzili, Said [1 ]
Chaoui, Allaoua [1 ]
Strecker, Martin [2 ]
Kerkouche, Elhillali [1 ,3 ]
机构：
[1] Univ Constantine 2 Abdelhamid Mehri, Comp Sci Dept, MISC Lab, Constantine, Algeria
[2] Univ Paul Sabatier, IRIT, Toulouse, France
[3] Univ Jijel, Comp Sci Dept, Jijel, Algeria
来源：
2017 IEEE 18TH INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IEEE IRI 2017) | 2017年
关键词：
UML SMD; Colored Petri nets (CPN); Model Transformation; Semantic correctness; Formal verification; Isabelle/HOL;
D O I：
10.1109/IRI.2017.63
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The Unified Modeling Language (UML) is a modeling language standardized by the OMG. The goal of UML is to supply software engineers, software developers, and system architects with tools for analysis, design, and implementation of software-based systems as well as for modeling business and similar processes. However, UML semantics is not formally defined. On the other hand, Colored Petri nets models (CPNs) are based on mathematical principle and have several verification capabilities. In this paper, we present another way to transform State Machine Diagrams (UML SMD) into Colored petri nets models and prove certain structural properties in this transformation itself. Therefore, we have described UML SMD (source model), Colored Petri nets (target model) and the transformation algorithm within Isabelle/HOL theorem prover. We demonstrate, also within Isabelle/HOL, that this transformation preserves certain structural properties for any input model (UML SMD).
引用
收藏
页码：419 / 426
页数：8
相关论文
共 21 条
  • [1] Ali T., 2007, 2007 IEEE INT MULT C, P1
  • [2] Amrani M, 2015, J OBJECT TECHNOL, V14, DOI 10.5381/jot.2015.14.1.a3
  • [3] Formalising concurrent UML state machines using coloured Petri nets
    Andre, Etienne
    Benmoussa, Mohamed Mahdi
    Choppy, Christine
    [J]. FORMAL ASPECTS OF COMPUTING, 2016, 28 (05) : 805 - 845
  • [4] Blech J O., 2005, Fujaba Days
  • [5] Cuadra JA, 2016, IEEE T SOFTWARE ENG, P1
  • [6] From UML Statecharts to LOTOS Expressions Using Graph Transformation
    Djaaboub, Salim
    Kerkouche, Elhillali
    Chaoui, Allaoua
    [J]. INFORMATION AND SOFTWARE TECHNOLOGIES, ICIST 2015, 2015, 538 : 548 - 559
  • [7] EL MILOUDI KHADIJA, 2015, MULTIVIEW APPROACH F
  • [8] Haftmann Florian, COD GEN IS HOL THEOR
  • [9] STATECHARTS - A VISUAL FORMALISM FOR COMPLEX-SYSTEMS
    HAREL, D
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1987, 8 (03) : 231 - &
  • [10] A UML and Colored Petri Nets Integrated Modeling and Analysis Approach using Graph Transformation
    Kerkouche, Elhillali
    Chaoui, Allaoua
    Bourennane, El Bay
    Labbani, Ouassila
    [J]. JOURNAL OF OBJECT TECHNOLOGY, 2010, 9 (04): : 25 - 43
123