III: Small: Specification and Analysis of Multi-Actor Data-Driven Business Processes

企业和其他组织越来越多地依赖于电子工作流作为业务流程的基础。这些工作流通常以数据库为中心，涉及执行不同角色的多个交互参与者。它们通常非常复杂，容易出现代价高昂的错误，这导致需要计算机辅助设计和分析工具。这些对于增强对复杂业务流程的健壮性和正确性的信心至关重要。该项目的总体目标是开发新的技术和工具，用于指定，分析，管理和优化复杂的数据驱动的业务流程，并明确关注多参与者设置。这包括数据共享和更新，为全球工作流程设计适合不同角色的参与者界面规范，以及互动参与者之间的合同义务规范。 它还将考虑运行时分析任务，包括关键全局属性的分布式监控，使用本地演员的意见，以推断有关全球工作流的信息，并验证自主离线部分工作流执行演员。该项目产生的技术和工具将增加对此类系统的稳健性和正确性的信心，并增强其功能和效率。 这将有利于各种各样的应用，如供应链管理、电子商务、数字政府和电子保健管理。该项目将通过培训研究生和本科生掌握对业务流程管理至关重要的尖端规范和静态分析技术，为人力资源开发做出贡献。 在软件验证的更广泛的背景下，目标是特别具有挑战性的，因为它们涉及无限状态系统的分析，而经典的软件验证通常处理有限状态抽象。 该项目将把最近为数据驱动工作流开发的技术扩展到多参与者场景，并深入了解规范语言的表现力和分析任务的易处理性之间的权衡。提出的技术问题是智力上的挑战，并将发挥技术从逻辑，自动机理论，计算复杂性，算法，和计算机辅助验证。http://db.ucsd.edu/nsf/actors

Businesses and other organizations increasingly rely on electronic workflows underlying business processes. These workflows are often centered around a database and involve multiple interacting actors carrying out different roles. They are typically very complex and prone to costly bugs, which leads to the need for computer-aided design and analysis tools. These are critical for increasing confidence in the robustness and correctness of complex business processes. The general objective of this project is to develop new techniques and tools for specifying, analyzing, managing, and optimizing complex data-driven business processes, with an explicit focus on the multi actor setting. This includes data sharing and updating, designing actor interface specifications to the global workflow tailored to different roles, and specification of contractual obligations among interacting actors. It will also consider runtime analysis tasks, including the distributed monitoring of critical global properties, the use of local actor observations to infer information about the global workflow, and validating autonomous offline partial workflow executions by actors. The techniques and tools resulting from this project will increase confidence in the robustness and correctness of such systems, and enhance their functionality and efficiency. This will benefit a wide variety of applications such as supply-chain management, e-commerce, digital government and electronic health-care management. The project will contribute to the development of human resources by training graduate and undergraduate students in cutting-edge specification and static analysis techniques which are crucial to business process management.Achieving the objectives of the project requires fundamental advances in our understanding of data-driven workflows involving multiple interacting actors. In the broader context of software verification, the goals are particularly challenging because they involve the analysis of infinite-state systems, whereas classical software verification typically deals with finite-state abstractions. The project will extend the techniques recently developed for data-driven workflows to the multi-actor scenario, and provide insight into the trade off between expressiveness of the specification language and tractability of analysis tasks. The technical problems raised are intellectually challenging, and will bring into play techniques from logic, automata theory, computational complexity, algorithms, and computer-aided verification.For further information see the project web site at: http://db.ucsd.edu/nsf/actors