Abstract: Aiming at the demand of location information modeling and analysis in mobile service process, a modeling and soundness verification method for location aware workflow was proposed by combining with existing workflow modeling method. Based on workflow net, this method used location constraints to describe the relationship between activities and location information with six primitives of describing location relationship. The method to verify the soundness for model was obtained based on reachability graph of Petri net. A location aware workflow modeling tool was developed based on ProM platform to verify the feasibility and validity of proposed method.

Key words: location aware workflow, modeling, location constraints, soundness verification, Petri nets

摘要： 针对移动业务过程中对位置信息建模和分析的需求，结合目前已有的工作流建模方法，提出一种针对位置敏感工作流进行建模和正确性验证的方法。该模型以工作流网为基础，结合6种描述位置之间关系的原语，以位置约束的形式定义业务流程中的位置信息及其与活动之间的关系，然后基于Petri网的状态可达图得出对所建立模型进行正确性检查的方法。基于ProM平台开发了一个位置敏感工作流的建模工具,验证了所提建模方法的可行性和算法的正确性。

关键词: 位置敏感工作流, 建模, 位置约束, 正确性验证, Petri网