面向语义约束的协同过程形式化建模与验证的研究

协同过程是"以人为本"的，协同过程的可信性以是否完成了人的协作目标来衡量。协同软件的新支撑环境是网格，核心技术是工作流，可信性保障手段是形式化验证。本课题研究网格环境下、面向协同应用的、大规模的、基于流程的、可信系统中面向语义约束的过程建模和验证。主要研究内容有：（1）扩展基于Petri网的网格工作流过程描述模型，增加控制流上的语义约束和描述分布式协同过程的方法。（2）突破结构验证的局限，研究协同验证的理论，提出协同验证的二维性，一个维度考虑规模，基于语义约束验证子模型的合成；一个维度考虑内容，基于语义约束验证协同目标的实现。（3）针对协同验证的新特性，分布式和动态性，提出有效、合理的在两个维度上交叉进行的验证过程。（4）基于化简技术，给出面向语义约束的完备的化简验证规则。本课题拟建立完善的协同过程建模和验证体系，特别是填补在验证理论和方法研究上的不足。