随着社会经济的快速发展,国家及各级地方政府对教育行业的投入越来越大,教育采购的规模也逐年扩大,这样需要一套信息化的措施来提高政府采购的执行效率。政府采购过程涉及单位众多,如何保证采购业务信息规范高效可控地流经各部门是采购过程信息化要解决的首要问题,而且采购业务信息与时间有紧密关系,比如标书发标之后的三天才可以投标等。这样对采购系统的的时间管理就有较高的要求。在工作流应用方面,随着企业竞争的日趋激烈,企业的业务过程也动态多变,要求控制业务信息实时地流经企业。这样原来的工作流系统已不适应现今的企业需求。时间信息的有效管理已经成为工作流技术推广应用的主要障碍,因此研究工作流的时间信息管理有重要意义。　　 本文基于协议采购系统研究如何有效地控制采购系统中的与业务相关的时间信息,协议采购系统是借助于工作流技术实现的。在工作流时间管理中,时间信息的建模、验证和分析是最基础、最核心的问题。为了解决协议采购系统中时间信息的建模和验证问题,引入了模型检测思想,利用模型检测技术来为协议采购系统的时间信息建模,提出了时钟Kripke迁移系统。时钟Kripke迁移系统是由Kripke迁移系统改进而来的,在原来模型的基础上增加了局部时钟和全局时钟,而且引入了特殊的迁移关系tick来表示时钟的运行,这样时钟Kripke迁移系统就可以用来建模工作流系统的时间信息。随后又分析了该模型相对于其他模型的优缺点。为了验证采购系统中的时间约束,首先提出了有效性的概念,给出了有效性约束的三种类型,然后利用时序逻辑CTL建立了有效性约束的模型。由于CTL的语义可以在状态迁移系统上进行解释,这样建模方法和验证方法就统一起来了。由于相关文献已经给出了工作流过程描述语言WPDL描述的工作流模型到Kripke迁移系统的转换方法,这样也就很容易建立基于时钟Kripke迁移系统的工作流模型,这就使得该方法更贴近于实用。最后给出了协议采购系统的一个实例,利用模型检测工具SMV验证了该实例的有效性约束,验证结果表明提出的方法是可行的。这样就把模型检测技术应用到了工作流系统中,对探索利用模型检测思想来对工作流时间信息建模与验证做了有益的尝试。