业务流程的自动化迫切要求一种流程描述语言能够描述现实场景下通过松耦合方式产生的业务流程。WS-CDL就是在这种需求下产生的一种基于编排的业务流程描述语言,其特点是不需要总体控制流程的执行顺序,仅需要通过约定参与者相互之间的交互方式即可实现流程的正常执行。这种方式具有结构灵活、流程定义模块可重用性高等特点,但是描述方式的灵活性所带来的缺点是导致流程中存在的问题难以发现。本文通过建立WS-CDL与形式化描述语言顺序通信进程(CSP)之间的映射关系,提出了一种从WS-CDL文档中自动抽象出业务流程的CSP模型的算法。通过该方法产生出的输出文件为可以直接通过计算机的CSP表达式,该表达式的内容与WS-CDL文档所描述的业务流程一致。该步工作实现了流程模型提取的自动化。建立业务流程数学模型的目的是为了验证流程的性质,发现流程中存在的问题。因此本文介绍了如何借助CSP表达式的特征行为和CSP的性质验证方法来验证业务流程的CSP模型的性质。使用这些验证方法可以通过结构分析和执行顺序推演实现对整个流程性质的分析。在本文的最后还介绍了如何借助CSP性质工具FDR2验证业务流程的相关性质,借助于这种方法可以实现对所建立CSP模型的性质自动化验证的目的使用本文建立的方法可以实现对WS-CDL所描述的业务流程的自动化建模和自动化验证所建立CSP模型的性质,同时本文也引入了使用人工推演的方法推演CSP模型的性质的方法。通过本文的介绍可以看出借助从WS-CDL文档中提出的CSP模型可以有效描述和验证业务流程的各种性质,这些工作为实现业务流程的自动化提供了有力保障。