建模与验证是业务过程生命周期管理中的重要环节。数据是业务过程的重要组成部分。现有业务过程建模语言都支持基于控制流维度进行数据建模。但是,在工作流中对数据进行形式化建模还存在很大挑战,进而影响在构造时对带有数据信息的工作流的形式化验证。本文通过扩展工作流网对工作流相关数据和应用数据进行了建模,在此基础上提出了数据感知的工作流合理性和一致性验证方法。本文主要工作包括：·给出了数据感知工作流网DWF-nets (Data-aware Workflow nets)的形式化定义,主要包括三部分：控制流、相关数据感知和应用数据感知。控制流采用工作流网描述；相关数据感知采用任务上分配变迁条件和任务上分配数据读写操作来描述,并重点从语法和语义两方面定义了具体的变迁条件；应用数据感知则在任务上不但标注数据操作同时也标注数据的状态对集合。区分了不同类型的数据与控制流之间的交互特征。·给出了一种数据感知工作流的合理性分析方法。在]DWF-nets理论基础之上,给出了在变迁条件影响下的行为语义。提出了一种符号可达分析方法验证]DWF-nets合理性属性。对可达分析面临的状态空间爆炸问题提出不同解决方案。·给出了一种数据感知工作流的一致性分析方法。在]DWF-nets基础之上提出一种集成工作流模型、业务对象生命周期的形式化建模方法。从语法和行为两方面形式化定义了工作流与业务对象生命周期的一致性要求。提出了“转换-合理性验证-行为一致性推导”的行为一致性的验证方法,并从理论上证明了该方法的正确性。上述方法已工具实现(作为分析插件集成到开源的过程验证框架ProM中),应用开发的工具对上述方法已进行全面评估。