Verification of Business Process Entailment Constraints Using SPIN

被引：0
|
作者：
Wolter, Christian [1 ]
Miseldine, Philip [1 ]
Meinel, Christoph [2 ]
机构：
[1] SAP Res, Vincenz Priessnitz Str 1, D-76131 Karlsruhe, Germany
[2] Univ Potsdam, HPI, IT Syst Engn, Potsdam, Germany
来源：
ENGINEERING SECURE SOFTWARE AND SYSTEMS, PROCEEDINGS | 2009年 / 5429卷
关键词：
Business Processes; Access Control; Verification; Model Checking; SPIN; BPMN;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The verification of access controls is essential for providing secure systems. Model checking is an automated technique used for verifying finite state machines. The properties to be verified are usually expressed as formula in temporal logic. In this paper we present an approach to verify access control security properties of a security annotated business process model. To this end we utilise a security enhanced BPMN notation to define access control properties. To enhance the usability the complex and technical details are hidden from the process modeller by using an automatic translation of the process model into a process meta language (Promela) based on Coloured Petri net (CPN) semantics. The model checker SPIN is used for the process model verification and a trace file is written to provide visual feedback to the modeller on the abstraction level of the verified process model. As a proof of concept the described translation methodology is implemented as a plug-in for the free web-based BPMN modelling tool Oryx.
引用
收藏
页码：1 / +
页数：4
相关论文
共 50 条
  • [21] A probabilistic method for business process verification: Reachability, Liveness and deadlock detection
    Naoum, Mohamed
    El Hichami, Outman
    Al Achhab, Mohammed
    El Mohajir, Badr eddine
    2016 4TH IEEE INTERNATIONAL COLLOQUIUM ON INFORMATION SCIENCE AND TECHNOLOGY (CIST), 2016, : 128 - 132
  • [22] Trends in business process analysis - From verification to process mining
    van der Aalst, Wil M. P.
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: HUMAN-COMPUTER INTERACTION, 2007, : IS13 - IS22
  • [23] Trends in business process analysis - From verification to process mining
    van der Aalst, Wil M. P.
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: SOFTWARE AGENTS AND INTERNET COMPUTING, 2007, : IS13 - IS22
  • [24] Trends in business process analysis - From verification to process mining
    van der Aalst, Wil M. P.
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: ARTIFICIAL INTELLIGENCE AND DECISION SUPPORT SYSTEMS, 2007, : IS13 - IS22
  • [25] Compliance verification of collaborative business process based on process abstraction
    Mo Q.
    Xiang J.
    Wang Y.
    Dai F.
    Xu X.
    Qi L.
    Jisuanji Jicheng Zhizao Xitong/Computer Integrated Manufacturing Systems, CIMS, 2021, 27 (09): : 2542 - 2555
  • [26] Formal Verification of Business Constraints in Workflow-Based Applications
    Stoica, Florin
    Stoica, Laura Florentina
    INFORMATION, 2024, 15 (12)
  • [27] Trends in business process analysis - From verification to process mining
    van der Aalst, Wil M. P.
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: INFORMATION SYSTEMS ANALYSIS AND SPECIFICATION, 2007, : IS13 - IS22
  • [28] Trends in business process analysis - From verification to process mining
    van der Aalst, Wil M. P.
    ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: DATABASES AND INFORMATION SYSTEMS INTEGRATION, 2007, : IS13 - IS22
  • [29] Verification of Common Business Rules in BPMN Process Models
    Rachdi, Anass
    En-Nouaary, Abdeslam
    Dahchour, Mohamed
    NETWORKED SYSTEMS, NETYS 2016, 2016, 9944 : 334 - 339
  • [30] Model checking and verification of the Internet Payment System with SPIN
    Zhang, Wei
    Ma, Wen-ke
    Shi, Hui-ling
    Zhu, Fu-qiang
    Journal of Software, 2012, 7 (09) : 1941 - 1949
12345