计算非线性抛物和双曲方程的有限差分方法.ppt

带数据工作流的形式化建模语言-数据感知的工作流网 刘续征 王朝霞，王建民，朱笑尘 清华大学软件学院，北京，100084 内容安排 研究背景与相关工作 论文工作 数据感知的工作流网 数据感知的工作流网的行为语义 总结与展望 研究领域－工作流 业务过程 研究动机－工作流形式化建模与验证的作用 .收集业务需求 .识别要求的活动 .识别需要的资源 .设计需处理的数据对象 .决定活动流逻辑 .设计工作流模型 .概念工作流模型转化为可执行工作流模型 .配置系统通用框架 .部署过程模型 .通过解释工作流模型 执行工作流实例 .监视过程执行 .分析过程日志 .可能的优化 工作流模型的质量是决定工作流系统成功的关键 相关工作－控制流维度建模与验证 van der Aalst教授提出工作流网WF-nets 工作流网的合理性属性(soundness) 相关工作－带数据工作流的建模与验证 带数据工作流的建模与验证 当前面临的挑战－带数据工作流的建模与验证 带数据工作流的形式化建模 未明确区分控制流与不同数据的关联特征； 数据表达能力较弱。 带数据工作流的形式化验证 形式化验证还停留在理论证明或不完备算法层次； 还未见到可支持工业界实际应用的验证工具。 内容安排 研究背景与相关工作 论文工作 数据感知的工作流网 数据感知的工作流网的行为语义 总结与展望 带数据工作流的形式化建模-数据分类 .描述控制流相关结构 .在工作流中未被定义，通过调用外部程序对其操作访问。 .既包括通用数据操作（如读或写），也包括与业务领域相关的特定操作（如PDM系统或PLM系统中的版本操作） .作为过程变量在工作流中定义 .被工作流引擎使用，例如路由条件变量等 .相关数据是应用数据在工作流中的映射 数据感知的工作流网-Data-aware Workflow nets(DWF-nets) 条件的形式化定义：一阶逻辑表达式，变量类型支持int,real和bool，操作符包括关系操作符，算术操作符与布尔操作符 10 数据感知的工作流网-Data-aware Workflow nets(DWF-nets) 数据感知的工作流网-Data-aware Workflow nets(DWF-nets) 数据感知的工作流网-Data-aware Workflow nets(DWF-nets) 内容安排 研究背景与相关工作 论文工作 数据感知的工作流网 数据感知的工作流网的行为语义 总结与展望 条件感知DWF-net的final marking集合(M=o) 条件感知DWF-net的行为语义 在 (p2, t1 t2 t3 t2)下，变迁t4能否使能？ 在 (p3, t1 t2 t3 t2 t4)下，变迁t5能否使能？ 条件感知DWF-net的行为语义 1 变迁序列（Transition Sequence) 2 变量更名（Variable Renaming） 3 变迁条件转换（Transition Condition Transformation） 条件感知DWF-net的行为语义 条件感知DWF-net-形式化验证 合理性验证(soundness verification ) 检测不可执行轨迹(detection of infeasible traces) 条件感知DWF-net-验证框架 条件感知DWF-net - 形式化验证 合理性验证(soundness verification ) 检测不可执行轨迹(detection of infeasible traces) • Zhaoxia Wang, Jianmin Wang, Xiaochen Zhu, and Lijie Wen. Verification of workflow nets with transition conditions. Journal of Zhejiang University- SCIENCE C(Computers and Electronics), 2012, 13(7):483-509. • Zhaoxia Wang, Lijie Wen, Xiaochen Zhu, Yingbo Liu, and Jianmin Wang. Detecting infeasible traces in business process models. ICEIS 2012 – Proceedings of the 14th International Conference on Enterprise Information Systems, Volume 3, Wroclaw, Poland, 26-30 June, 2012, 139-144. 对象操作感知 DWF-net的marking (