In order to describe the temporal aspect of workflow model and verify the temporal consistency,a method based on temporal logic and model checking for modeling and verifying time constraint workflows is presented.By this method,the first order logic is used to model workflow including its basic temporal information, temporal logic is used to model the time constraints,and model checking is used to analyze and verify the temporal consistency.The method can be used to verify any time constraints that can be described by temporal logic.Also the method can offer a counterexample of workflow instance to the time constraint which can not pass the verification. Finally,the method is validated through a case study.
[1]Fan YS.Fundamentals of Workflow Management Technology.Beijing:Tsinghua University Press/Springer-Verlag,2001.5-22 (in Chinese).
[2]Li HF,Fan YS.Overview on managing time in workflow systems.Journal of Software,2002,13(8):1552-1558 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/13/1552.pdf
[3]Eder J,Panagos E,Rabinovich M.Time constraints in workflow systems.In:Jarke M,Oberweis A,eds.Proc.of the 11th Conf.on Advanced Information Systems Engineering.Heidelberg:Springer-Verlag,1999.286-300.
[4]Eder J,Panagos E,Pozewaunig H,Rabinovich M.Time management in workflow systems.In:Abramowicz W,Orlowska ME,eds.Proc.of the 3rd Int'l Conf.on Business Information Systems.Berlin:Springer-Verlag,1999.265-280.
[5]Bowden FD.A brief survey and synthesis of the roles of time in Petri nets.Mathematical and Computer Modeling,2001,31(3):55-86.
[6]Serthomieu B,Diaz M.Modeling and verification of time dependent systems using time Petri nets.IEEE Trans.on Software Engineering,1991,17(3):259-273.
[7]Tsai J,Yang SJ.Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications.IEEE Trans.on Software Engineering,1995,21(1):32-49.
[8]Sadiq W,Orlowska ME.Analyzing process models using graph reduction techniques.Information System,2000,25(2):117-134.
[10]Kifer M,Subrahmanian VS.Theory of generalized annotated logic programming and its applications.Journal of Logic Programming,1992,12(4):1-33.
[11]Holzmann GJ.The model checker SPIN.IEEE Trans.on Software Engineering,1997,23(5):279-295.
[12]Cleavel R,Parrow J,Steffen B.The concurrency workbench:A semantics based verification tool for the verification of concurrent systems.ACM Trans.on Programming Languages and Systems,1993,5(1):36-72.