随着业务流程模型的广泛应用,其正确性显得尤为重要。时间约束决定了业务流程能否正确执行,任何一点时间延迟都有可能造成极大的资源浪费,所以对时间约束进行验证是检测业务流程模型正确性非常重要的环节。本文以时间模式分析为基础,研究了基于时间模式分析的业务流程模型验证方法,具体工作如下:首先,提出了基于形式化语义的时间模式分析方法。根据业务流程模型中常见的时间约束类型将时间模式分为持续时间模式、固定时刻模式与周期循环模式三类,给出了业务流图、时间区间以及三类时间模式的形式化描述。定义了时间模式的可满足性,提出了周期循环模式到持续时间模式的转换规则,证明了可满足性保持定理,即业务流图满足周期循环模式当且仅当满足转换后的持续时间模式。其次,提出了基于时间模式分析的业务流程模型验证方法。针对业务流程模型的结构、行为、流程等一致性问题提出了验证框架,基于时间模式分析设计了业务流程模型静态结构、动态行为和业务流图到Prolog的转换规则与转换算法,以及静态结构一致性、动态行为一致和时间模式一致性到Prolog的转换规则。以医疗流程模型为例进行了模型一致性验证和修复。与相关工作对比表明本文的方法可以全面地验证业务流模型一致性。最后,基于业务流程模型时间模式分析与一致性验证方法设计实现了业务流程模型验证平台。该平台以GMF为基础,设计了业务流程模型建模模块、静态结构与动态行为验证模块以及业务流图验证模块,实现了从业务流程模型建模到模型的静态结构一致性、动态行为一致性以及时间模式一致性的自动验证功能。以高铁订票系统为例进行了模型建模和一致性验证。结果表明平台设计能够满足业务流程模型的建模以及一致性的验证需求。