业务流程管理BPM(Business Process Management)综合集成了企业的任务、资源和数据,并通过对这些流程的管理帮助企业灵活、敏捷地应对外部环境的变化。业务流程建模是BPM中最为重要的环节,它直接决定了整个管理工作对业务需求的把握程度。实践表明,BPMN(Business Process Modeling Notation)是一种标准的、易于使用的业务流程建模语言。BPMN不仅提供了简单的建模手段,也提供了表达业务流程的丰富语义。业界的业务流程建模方法仅限于对流程的描述,缺少业务流程模型的验证,因此无法保证业务流程模型在理解需求和系统设计方面的正确性和可靠性,限制了业务流程模型按照自顶向下的方式在实践中的普及和应用。针对这一问题,本文提出了一种检验业务流程模型的技术路线,开发了模型转换工具,用于验证流程模型的正确性。这一技术路线引入W3C规范WS-CDL(Web ServicesChoreography Description Language),作为一个承上启下的流程模型表达。本文分析了BPMN和WS-CDL两种建模语言的特征,建立了彼此相互转换的映射关系和算法。从用户易于使用的BPMN,转换为WS-CDL表达的服务编排,然后,应用Pi-演算对服务编排形式化,应用Pi-演算验证工具对形式化模型进行检验和判定,从而保证了业务流程模型不存在冲突和死锁等问题。本文开发的转换工具BPMN2CDL,证实了技术路线的可行性。总之,本文的研究成果支持在模型设计阶段就进行形式化分析和验证,有效提高建模质量,降低软件系统开发的风险,减少由于模型错误导致的反复代价,保证了业务流程模型的可靠性与健壮性。