摘要
在使用Petri网构建工作流行为结构模型的同时,使用时态逻辑描述工作流模型的需求与特性,则具有描述能力强、灵活方便的优点。在此基础上,综合考虑时态逻辑列表法和即时验证方法的特点,给出一种主要利用B櫣chi自动机进行工作流模型需求及特性验证的方法,提高了工作流模型的合理性和可靠性。最后,验证分析了电子商务的工作流实例。
Using the Petri net to build the behavioral model of workflow, the temporal logic is used to specify the requirements and properties of the workflow model. This method has more descriptive power and is flexible,easy to be used. Based on the tableau and on-the-fly methods of temporal logic, a realization method that mainly uses the Büchi automata to validate the workflow model is presented. It improves the rationality and reliability of the workflow model. Finally, a workflow case of electronic commerce is analyzed and validated.
关键词
工作流
时态逻辑
模型
workflow
temporal logic
model
