Security Validation of Business Processes via Model-Checking

被引:0
|
作者
Arsac, Wihem [1 ]
Compagna, Luca [1 ]
Pellegrino, Giancarlo [1 ]
Ponta, Serena Elisa [1 ]
机构
[1] SAP Res Sophia Antipolis, F-06250 Mougins, France
来源
关键词
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
More and more industrial activities are captured through Business Processes (BPs). To evaluate whether a BP under-design enjoys certain security desiderata is hardly manageable by business analysts without tool support, as the BP runtime environment is highly dynamic (e.g., task delegation). Automated reasoning techniques such as model checking can provide the required level of assurance but suffer of well-known obstacles for the adoption in industrial systems, e.g. they require a strong logical and mathematical background. In this paper, we present a novel security validation approach for BPs that employs state-of-the-art. model checking techniques for evaluating security-relevant aspects of BPs in dynamic environments and offers accessible user interfaces and apprehensive feedback for business analysts so to be suitable for industry.
引用
收藏
页码:29 / 42
页数:14
相关论文
共 50 条
  • [41] Model checking authorization requirements in business processes
    Armando, Alessandro
    Ponta, Serena Elisa
    [J]. COMPUTERS & SECURITY, 2014, 40 : 1 - 22
  • [42] Robust Model-Checking of Timed Automata via Pumping in Channel Machines
    Bouyer, Patricia
    Markey, Nicolas
    Sankur, Ocan
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2011, 6919 : 97 - +
  • [43] Utility, sensitivity analysis, and cross-validation in Bayesian model-checking - Comment
    Hill, BM
    [J]. STATISTICA SINICA, 1996, 6 (04) : 767 - 773
  • [44] Model-Checking HyperLTL for Pushdown Systems
    Pommellet, Adrien
    Touili, Tayssir
    [J]. MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 133 - 152
  • [45] Model-checking Timed Temporal Logics
    Bouyer, Patricia
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
  • [46] A tool for model-checking Markov chains
    Holger Hermanns
    Joost-Pieter Katoen
    Joachim Meyer-Kayser
    Markus Siegle
    [J]. International Journal on Software Tools for Technology Transfer, 2003, 4 (2) : 153 - 172
  • [47] Connectivity testing through model-checking
    Godskesen, JC
    Nielsen, B
    Skou, A
    [J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2004, PROCEEDINGS, 2004, 3235 : 167 - 184
  • [48] Foundations of incremental aspect model-checking
    Krishnamurthi, Shriram
    Fisler, Kathi
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
  • [49] Model-checking TRIO specifications in SPIN
    Morzenti, A
    Pradella, M
    San Pietro, P
    Spoletini, P
    [J]. FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
  • [50] A Model-Checking Tool for Families of Services
    Asirelli, Patrizia
    ter Beek, Maurice H.
    Fantechi, Alessandro
    Gnesi, Stefania
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 44 - 58