III: Small: Data-Centric Business Processes: Specification and Static Analysis

企业和其他组织越来越依赖于业务流程管理，特别是对业务流程底层的电子工作流的管理。这些工作流通常以数据库为中心。它们通常非常复杂，容易产生代价高昂的错误，这导致了对计算机辅助设计和静态分析工具的迫切需求。这些工具将增强功能，并增加对复杂业务流程的稳健性和正确性的信心。 它们将潜在地使各种各样的应用受益，从电子商务到数字政府，再到医疗保健和科学应用。适用于静态分析的经典软件验证技术包括模型检查和定理证明。然而，这两种方法都有严重的局限性：模型检查需要有限状态抽象，这会导致业务流程和已验证属性的语义严重丢失。定理证明是不完整的，需要专家用户的反馈。本项目提出了一种静态分析的替代方法.它的目的不是应用只有部分成功保证的通用技术，而是识别受限制但具有足够表达力的业务流程类，可以以全自动的方式进行完整的静态分析。此外，与传统的以流程为中心的工作流相比，验证的目标是语义丰富的数据感知工作流。数据感知是上述应用程序中的一个重要特征，最近导致了一种新的工作流规范方法的出现，其中数据是突出的。这种方法是由IBM引入的，它关注的是数据记录，即所谓的“业务工件”或简称为“工件”，它对应于关键的业务相关对象、它们的生命周期以及在工件上调用的服务（或任务）。IBM的以工件为中心的方法已经被证明可以对中型和大型企业的运营产生实质性的改进。本项目的主要目标是开发新的工具，用于高级规范和验证以数据为中心的业务流程。该项目研究了规范语言的表达能力和分析任务的可行性之间的权衡。它的目的是建立静态分析的易处理性边界，并开发实用的算法和算法。将开发用于执行分析任务的工具，这些工具将与Siena集成，Siena是IBM用于将以工件为中心的业务流程规范编译为工作流支持代码的原型。所提出的技术问题在智力上相当具有挑战性，并从逻辑、自动机理论、计算复杂性、算法和计算机辅助验证等方面发挥技术作用。由此产生的静态分析工具有很大的潜力成为业务流程领域的一项变革性技术。有关详细信息，请参阅项目网页db.ucsd.edu/artifacts

Businesses and other organizations increasingly rely on businessprocess management, and in particular the management of electronicworkflows underlying business processes. These workflows are oftencentered around a database. They are typically very complex and proneto costly bugs, which leads to a critical need for computer-aideddesign and static analysis tools. Such tools would result in enhancedfunctionality, as well as increased confidence in the robustness andcorrectness of complex business processes. They would potentiallybenefit a wide variety of applications ranging from e-commerce todigital government to healthcare and scientific applications. Classical software verification techniques applicable to static analysis include model checking and theorem proving. However, both have seriouslimitations: Model checking requires finite-state abstraction, whichresults in serious loss of semantics for both the business process andverified properties. Theorem proving is incomplete and requires expertuser feedback. This project proposes an alternative approach tostatic analysis. Instead of applying general-purpose techniques withonly partial guarantees of success, it aims to identify restricted butsufficiently expressive classes of business processes for which soundand complete static analysis can be performed in a fully automatic way.Moreover, the target of verification consists of semantically richdata-aware workflows, in contrast to the traditional process-centricworkflows. Data awareness is a feature of central importance inapplications such as the above, which has recently led to theemergence of a new approach to workflow specification in which data ispre-eminent. This approach, introduced by IBM, focuses on data records,known as "business artifacts" or simply "artifacts", that correspondto key business-relevant objects, their life cycles, and theservices (or tasks) that are invoked on the artifacts.IBM's artifact-centric approach has been demonstrated to yieldsubstantial improvements to the operations of medium- and large-sizedbusinesses. The main objective of the present project is to developnew tools for the high-level specification and verification of suchdata-centric business processes. The project investigates thetrade-offs between the expressiveness of the specification languageand the feasibility of the analysis tasks. It aims to establishtractability boundaries for static analysis and to develop practicalalgorithms and heuristics. Tools are to be developed for carrying outanalysis tasks, that will be integrated with Siena, IBM's prototypefor compiling artifact-centric business process specifications intoworkflow support code. The technical problems raised areintellectually quite challenging, and bring into play techniques fromlogic, automata theory, computational complexity, algorithms, andcomputer-aided verification. The resulting static analysis tools havehigh potential for becoming a transformational technology in the areaof business processes.For further information see the project web pagehttp://db.ucsd.edu/artifacts