Proposal of Formal Verification of Selected BPMN Models with Alvis Modeling Language

被引:0
|
作者
Szpyrka, Marcin [1 ]
Nalepa, Grzegorz J. [1 ]
Ligeza, Antoni [1 ]
Kluza, Krzysztof [1 ]
机构
[1] AGH Univ Sci & Technol, PL-30059 Krakow, Poland
来源
关键词
SYSTEMS;
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
BPMN is a leading visual notation for modeling business processes. Although there is many tools that allows for modeling using BPMN, they mostly do not support formal verification of models. The Alvis language was developed for modeling and verification of embedded systems. However, it is suitable for the modeling of any information systems with parallel subsystems. The goal of this paper is to describe the concept of using Alvis for a formal verification of selected BPMN models. In the paper a translation from BPMN to Alvis model is proposed. The translation is discussed and evaluated using a simple yet illustrative example.
引用
收藏
页码:249 / 255
页数:7
相关论文
共 50 条
  • [1] Discrete-Time Systems Modeling and Verification With Alvis Language and Tools
    Szpyrka, Marcin
    Wypych, Michal
    Biernacki, Jerzy
    Podolski, Lukasz
    [J]. IEEE ACCESS, 2018, 6 : 78766 - 78779
  • [2] Formal Semantics and Verification of BPMN Transaction and Compensation
    Takemura, Tsukasa
    [J]. 2008 IEEE ASIA-PACIFIC SERVICES COMPUTING CONFERENCE, VOLS 1-3, PROCEEDINGS, 2008, : 284 - 290
  • [3] Formal Description of Alvis Language with α0 System Layer
    Szpyrka, Marcin
    Matyasik, Piotr
    Mrowka, Rafal
    Kotulski, Leszek
    [J]. FUNDAMENTA INFORMATICAE, 2014, 129 (1-2) : 161 - 176
  • [4] Assessing business process models: a literature review on techniques for BPMN testing and formal verification
    Lopes, Tomas
    Guerreiro, Sergio
    [J]. BUSINESS PROCESS MANAGEMENT JOURNAL, 2023, 29 (08) : 133 - 162
  • [5] Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN
    Calvanese, Diego
    Ghilardi, Silvio
    Gianola, Alessandro
    Montali, Marco
    Rivkin, Andrey
    [J]. BUSINESS PROCESS MANAGEMENT (BPM 2019), 2019, 11675 : 157 - 175
  • [6] Formal Definition of Measures for BPMN Models
    Reynoso, Luis
    Rolon, Elvira
    Genero, Marcela
    Garcia, Felix
    Ruiz, Francisco
    Piattini, Mario
    [J]. SOFTWARE PROCESS AND PRODUCT MEASUREMENT, PROCEEDINGS, 2009, 5891 : 285 - +
  • [7] Proposal for incremental formal verification
    Shonai, T
    Matsumoto, K
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1998, E81D (11) : 1172 - 1185
  • [8] Data flow modeling and verification of complex BPMN collaboration models based on HCPN
    Huang, Fenglan
    Ni, Feng
    Liu, Jiang
    Tao, Mengyi
    Zhou, Yining
    Li, Yexun
    [J]. Jisuanji Jicheng Zhizao Xitong/Computer Integrated Manufacturing Systems, CIMS, 2024, 30 (05): : 1754 - 1769
  • [9] A formal approach for the analysis of BPMN collaboration models
    Corradini, Flavio
    Fornari, Fabrizio
    Polini, Andrea
    Re, Barbara
    Tiezzi, Francesco
    Vandin, Andrea
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2021, 180
  • [10] A Formalization Proposal of Timed BPMN for Compositional Verification of Business Processes
    Mendoza Morales, Luis E.
    Capel Tunon, Manuel I.
    Perez, Maria A.
    [J]. ENTERPRISE INFORMATION SYSTEMS, 2011, 73 : 388 - +