Modelling and model checking suspendible business processes via statechart diagrams and CSP

被引：6
|
作者：
Yeung, W. L. [1 ]
Leung, K. R. P. H.
Wang, Ji
Dong, Wei
机构：
[1] Lingnan Univ, Dept Comp & Decis Sci, Hong Kong, Hong Kong, Peoples R China
[2] Hong Kong Inst Vocat Educ, Dept Informat & Commun Technol, Hong Kong, Hong Kong, Peoples R China
[3] Natl Lab Parallel & Distributed Proc, Changsha, Hunan, Peoples R China
来源：
SCIENCE OF COMPUTER PROGRAMMING | 2007年 / 65卷 / 01期
基金：
中国国家自然科学基金;
关键词：
statechart diagrams; history mechanism; object behaviour; process modelling; model checking;
D O I：
10.1016/j.scico.2006.08.007
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
When modelling object behaviour with UML statechart diagrams, the history mechanism can be useful for modelling the suspension of a "normal" business process upon certain "abnormal" events together with the subsequent resumption, as illustrated by the examples in this paper. However, previous approaches to model checking statechart diagrams often ignore the history mechanism. We enhanced such a previous approach based on Communicating Sequential Processes (CSP) and developed a support tool for it. (c) 2006 Elsevier B.V. All rights reserved.
引用
收藏
页码：14 / 29
页数：16
相关论文
共 29 条
  • [1] Symbolic model checking of UML statechart diagrams with an integrated approach
    Lam, VSW
    Padget, J
    [J]. 11TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOP ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2004, : 337 - 346
  • [2] A CSP-theoretic framework of checking conformance of Business Processes
    Roy, Suman
    Bihary, Sidharth
    Laos, Jose Alfonso Corso
    [J]. 2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 2012, : 30 - 39
  • [3] Security Validation of Business Processes via Model-Checking
    Arsac, Wihem
    Compagna, Luca
    Pellegrino, Giancarlo
    Ponta, Serena Elisa
    [J]. ENGINEERING SECURE SOFTWARE AND SYSTEMS, 2011, 6542 : 29 - 42
  • [4] Formalization and Model Checking of SysML State Machine Diagrams by CSP#
    Ando, Takahiro
    Yatsu, Hirokazu
    Kong, Weiqiang
    Hisazumi, Kenji
    Fukuda, Akira
    [J]. COMPUTATIONAL SCIENCE AND ITS APPLICATIONS (ICCSA 2013), PT III, 2013, 7973 : 114 - 127
  • [5] Model checking authorization requirements in business processes
    Armando, Alessandro
    Ponta, Serena Elisa
    [J]. COMPUTERS & SECURITY, 2014, 40 : 1 - 22
  • [6] Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking
    Gnesi, S
    Latella, D
    Massink, M
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2002, 51 (01): : 43 - 75
  • [7] Model Checking of Security-Sensitive Business Processes
    Armando, Alessandro
    Ponta, Serena Elisa
    [J]. FORMAL ASPECTS IN SECURITY AND TRUST, 2010, 5983 : 66 - 80
  • [8] Formal Verification of Business Processes using Model Checking
    Stoica, Florin
    [J]. INNOVATION MANAGEMENT AND EDUCATION EXCELLENCE VISION 2020: FROM REGIONAL DEVELOPMENT SUSTAINABILITY TO GLOBAL ECONOMIC GROWTH, VOLS I - VI, 2016, : 2563 - 2575
  • [9] Model Checking Analysis of Semantically Annotated Business Processes
    Jose Ibanez, Maria
    Fabra, Javier
    Alvarez, Pedro
    Ezpeleta, Joaquin
    [J]. IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2012, 42 (04): : 854 - 867
  • [10] Compositional Verification of Business Processes by Model-Checking
    Mendoza, Luis E.
    Capel, Manuel I.
    Perez, Maria
    [J]. MSVVEIS 2010: MODELLING, SIMULATION, VERIFICATION AND VALIDATION OF ENTERPRISE INFORMATION SYSTEMS, 2010, : 60 - 69
123