BPMN是软件开发领域中较为常用的描述业务流程的建模标准。在包含业务流程可变性的软件产品线中,基于BPMN的业务流程模板可支持针对领域需求的业务流程描述,并且能够高效地生成面向特定应用需求的业务流程实例。然而,由于业务流程模版的设计往往是基于设计师的经验,缺少形式化的验证方法,因而领域需求与业务流程模板之间经常存在不一致情况。领域需求与业务流程模版间的不一致性通常有两种情况,一方面是领域需求本身的缺陷,这可能是由于需求分析不足或者分析人员的疏忽所造成的(例如,遗漏需求依赖关系等)；另一方面是业务流程的设计与领域需求的矛盾,这通常是由于设计者对需求理解不足或者设计疏忽所造成的(例如,采用错误的图元元素描述流程)。针对该问题,本文提出一种面向领域需求与业务流程一致性的模型检测方法,该方法首先形式化的定义了领域需求,这个过程使用变数线性时态逻辑(FLTL)来抽取业务流程中需要验证的流程特性；之后,将BPMN流程实例通过一定的映射规则,转换成有限状态进程公式(FSP),该过程能够将业务流程有效地转换成有限状态自动机,从而进行验证；然后,使用自动化模型检测工具发现领域需求与业务流程之间的不一致,这将输出一个反例(发生错误的状态迁移路径)及其所违反的业务流程特性,并将这些结果反馈给相关人员实施修正；最后,本文还讨论了不一致性错误在该模型检测方法中的体现,及相应的修改方案。