基于线性时序逻辑的业务流程验证

The model checking of business process based on linear temporal logic

目的为了解决业务流程设计与需求的不一致性问题。方法提出了一种基于XML过程定义语言和线性时序逻辑的业务流程验证方法。结果采用Promela语言描述业务流程模型,线性时序逻辑表示抽象的业务需求,通过模型检测器Spin完成流程的验证工作。结论实现了对流程正确性的判断。

Aim To resolve the inconsistency between business process design and requirements.Methods A novel method is proposed,which is based on XML process definition language and linear temporal logic.Results Promela is used to describe the model of the business process,and the linear temporal logic gives the Abstract description of the business requirements.Spin model checker presents the verification results.Conclusion This method can determine the correctness of the business process.