关键词: 协同业务过程, 领域约束, 符合性, 模型检测, 弱轨迹等价

Abstract: Verifying the compliance between collaborative business processes and domain constraints is a key issue.However,the existing work ignores the detailed processing of internal processes,leading to the disclosure of organizational internal process information,misconduct of compliance verification,and low verification efficiency.For this reason,a method for verifying the compliance between collaborative business processes and domain constraints based on the process abstraction was proposed.The label transition system and the compliance language Compliance Request Language (CRL) was used to describe the business process and domain constraints respectively.All the internal process details in the business processes based on the weak trace equivalence was removed to get the abstract business processes,which were combined to obtain the abstract collaborative business process.The model checking technology was used to automatically verify the compliance between collaborative business process with the domain constraints.The compliance verification of collaborative business process was transformed into the compliance verification of the abstract collaborative business process,which could effectively avoid exposing the internal process information of the organization,ensure the correctness of the compliance verification results and improve the efficiency of formal verification.To illustrate the effectiveness of the proposed method,the actual collaborative business process set was used to conduct experiments and to evaluate from the analysis efficiency.The experimental results showed that the proposed method was more effective in analyzing the conformity of the collaborative business process and domain constraints compared with the existing work.

Key words: collaborative business processes, domain constraints, compliance, model checking, weak trace equivalence