TOWARDS FORMAL AND DEDUCTION-BASED ANALYSIS OF BUSINESS MODELS FOR SOA PROCESSES

被引：13
作者：
Klimek, Radoslaw [1 ]
机构：
[1] AGH Univ Sci & Technol, PL-30059 Krakow, Poland
来源：
ICAART: PROCEEDINGS OF THE 4TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE, VOL. 2 | 2012年
关键词：
Business models; BPMN; SOA and software agents; Formal verification; Deductive reasoning; Semantic tableaux; Temporal logic; Workflow design patterns; Generating specifications;
D O I：
10.5220/0003740503250330
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The paper concerns formal analysis and verification of business models expressed in BPMN as a visualization of SOA processes. This verification is based on deductive reasoning which is in a certain kind of opposition to the well-known approaches based on state exploration (model checking). Semantic tableaux arc proposed as a method of inference. Both the logical specification and the desired system properties are expressed in the smallest linear temporal logic. Automatic transformations of business models (expressed as workflow patterns) to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. An algorithm for generation of a logical specification is presented.
引用
收藏
页码：325 / 330
页数：6
相关论文
共 17 条
  • [1] A SYSTEM FOR DEDUCTION-BASED FORMAL VERIFICATION OF WORKFLOW-ORIENTED SOFTWARE MODELS
    Klimek, Radoslaw
    INTERNATIONAL JOURNAL OF APPLIED MATHEMATICS AND COMPUTER SCIENCE, 2014, 24 (04) : 941 - 956
  • [2] Deduction-Based Formal Verification of Requirements Models with Automatic Generation of Logical Specifications
    Klimek, Radoslaw
    EVALUATION OF NOVEL APPROACHES TO SOFTWARE ENGINEERING, ENASE 2012, 2013, 410 : 157 - 171
  • [3] From Extraction of Logical Specifications to Deduction-Based Formal Verification of Requirements Models
    Klimek, Radoslaw
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2013, 2013, 8137 : 61 - 75
  • [4] A Deduction-based System for Formal Verification of Agent-ready Web Services
    Klimek, Radoslaw
    ADVANCED METHODS AND TECHNOLOGIES FOR AGENT AND MULTI-AGENT SYSTEMS, 2013, 252 : 203 - 212
  • [5] An infrastructure virtualisation SOA for VNO-based business models
    Nepal, Surya
    Chan, Jonathan
    Chen, Shiping
    Moreland, David
    Zic, John
    2007 IEEE INTERNATIONAL CONFERENCE ON SERVICES COMPUTING, PROCEEDINGS, 2007, : 44 - +
  • [6] Semi-formal transformation of secure business processes into analysis class and use case models: An MDA approach
    Rodriguez, Alfonso
    Garcia-Rodriguez de Guzman, Ignacio
    Fernandez-Medina, Eduardo
    Piattini, Mario
    INFORMATION AND SOFTWARE TECHNOLOGY, 2010, 52 (09) : 945 - 971
  • [7] Towards a Component-based Description of Business Models: A State-of-the-Art Analysis
    Krumeich, Julian
    Burkhart, Thomas
    Werth, Dirk
    Loos, Peter
    AMCIS 2012 PROCEEDINGS, 2012,
  • [8] Formal verification of complex business processes based on high-level Petri nets
    Kheldoun, Ahmed
    Barkaoui, Kamel
    Ioualalen, Malika
    INFORMATION SCIENCES, 2017, 385 : 39 - 54
  • [9] Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach
    Garfatta, Ikram
    Klai, Kais
    Graiet, Mahamed
    Gaaloul, Walid
    SERVICE-ORIENTED COMPUTING, ICSOC 2020, 2021, 12632 : 47 - 53
  • [10] Towards a Web-Based Platform Supporting the Recomposition of Business Processes
    Wisniewski, Piotr
    Bujak, Agata
    Kluza, Krzysztof
    Suchenia, Anna
    Zaremba, Mateusz
    Jemiolo, Pawel
    Ligeza, Antoni
    INFORMATION TECHNOLOGY FOR MANAGEMENT: BUSINESS AND SOCIAL ISSUES, ISM 2021, 2022, 442 : 166 - 185
12