本文首先综述了当前工作流模型及其验证方法,着重介绍了基于Petri网进行工作流建模和验证的优缺点,然后提出了一个基于双分支条件有向图(Double-Road Conditional Directed Graph(DCDG))的工作流模型,该模型是一个工作流实际业务流程的抽象,它建立在状态图和ECA规则的基础上,具有较强的表达力和直观的图形描述,同时底层通讯机制基于对象和ECA规则,便于进行语义化描述.工作流模型正确性验证问题是工作流研究领域中的一个重要问题,工作流管理系统可能建立错误的工作流模型,导致工作流的执行出现异常.有的研究者将事件平衡分析方法引入了工作流模型,通过分析局部工作流的控制逻辑,提出了验证工作流控制逻辑正确性的一个必要条件,但是并没有涉及到如何解决整个工作流的控制逻辑正确性验证问题.本文在基于双分支条件有向图的工作流模型基础上,提出了一种验证整个工作流控制逻辑正确性的方法,实验结果表明,该方法是可行的.工作流管理系统中的时间管理问题是工作流研究领域中另一个重要的问题,通过对工作流活动加以时间约束,可以保证工作流正确、高效的执行.目前,许多研究者对工作流模型中时间属性进行建模,进行了一些有益的工作,但是对于工作流活动时间约束的正确性验证问题和时序逻辑的推理问题没有深入的讨论.本文首先分析了工作流管理系统中主要应该考虑的时间问题,然后在双分支条件有向图模型基础上进行了一些关于时序逻辑推理问题的研究,提出了四个推理规则,同时提出了验证工作流活动时间约束正确性的一些必要条件.另外,本文提出了一个基于对象的工作流活动定义,在此基础上引入了ECA规则,作为对象消息通讯的基础.最后,我们将本文提出的验证思想用于实际的电子政务软件开发中,分析设计了正确的业务工作流控制模型和组织模型,进行了有益的尝试.