数据感知业务流程验证与执行一致性估计

### 数据感知业务流程验证与执行一致性估计 在当今的业务流程管理领域，数据的重要性日益凸显。一方面，需要对数据感知的业务流程进行形式化建模和验证，以确保其安全性和正确性；另一方面，随着事件数据量的不断增加，如何高效地估计业务流程执行的一致性成为了一个关键问题。 #### 数据感知业务流程（DAB）的验证 ##### 验证问题的提出 对于数据感知业务流程（DAB），需要一种语言来表达其不安全属性。这些属性是在DAB的数据集 \(D\) 和流程 \(P\) 上定义的，具体是定义6中保护语言的一个片段，它可以查询存储库关系、案例变量以及这些关系所引用的分类关系，同时还能查询流程 \(P\) 的控制状态。通过隐式地在 \(D\) 中扩展额外的特殊案例控制变量，来表示 \(P\) 中各个块的生命周期状态。 例如，对于一个招聘流程，我们可以定义属性来检查流程是否可以终止，或者在某些操作后是否会出现不符合预期的情况。 ```mermaid graph LR classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; A(开始):::process --> B(接收申请):::process B --> C(评估申请):::process C --> D{是否通过}:::process D -->|是| E(选择获胜者):::process D -->|否| F(结束):::process E --> F ``` ##### 属性的定义 一个关于 \(M = \langle D, P \rangle\) 的属性是一个在 \(D\) 和 \(P\) 的控制变量上的保护 \(G\)，其中 \(G\) 中的每个非案例变量也必须出现在一个关系原子 \(R(y_1, \ldots, y_n)\) 中，这里 \(R\) 要么是存储库关系，要么是分类关系且 \(y_1 \in D.cvars\)。 例如，属性 \((HPlifecycle = completed)\) 可以检查招聘流程的某个案例是否可以终止；属性 \(EvalApplifecycle = completed \land Application(j, u, s, true) \land s > 100\) 描述了在评估申请后，存在得分大于100的申请人这一不期望的情况。 ##### DAB到基于数组的工件系统的转换 为了验证DAB的不安全属性，我们将其编码为基于数组的工件系统（RAS）的不安全验证问题。具体来说，\(D.cat\) 和 \(D.cvars\) 分别映射到RAS的只读数据库和工件变量；\(D.repo\) 则通过为每个存储库关系 \(R\) 和其属性 \(a\) 引入一个专用数组来编码，数组索引表示 \(R\) 中元组的隐式标识符。案例变量使用大小为1的（有界）数组表示。 在此基础上，将流程 \(P\) 转换为RAS的转换公式，以精确重构 \(P\) 中各个块的执行语义。 ##### 验证结果 - **BackReach过程**：定义了BackReach作为反向可达性过程，它接受一个DAB \(M\)、待验证的属性 \(\phi\)、表示 \(M\) 是否为存储库有界的布尔值以及表示插入语义是集合还是多重集的布尔值作为输入。首先将 \(M\) 转换为对应的RAS \(M'\)，将 \(\phi\) 转换为 \(M'\) 上的属性 \(\phi'\)，然后调用mcmt反向可达性过程对 \(M'\) 和 \(\phi'\) 进行验证并返回结果。 - **验证定理** - **定理1**：BackReach对于使用多重集或集合插入语义的DAB的不安全检查是可靠且完备的。这意味着当BackReach终止时，它会给出正确的答案；并且只要DAB相对于某个属性是不安全的，BackReach就能检测到。