工作流时序约束模型分析与验证方法
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant No.60274046 (国家自然科学基金)


A Method of Time Constraint Workflow Model Analysis and Verification
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [14]
  • |
  • 相似文献 [20]
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.

    Abstract:

    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.
    [9]Edmund M,Clarke J,Orna G,Doron AP.Model Checking.Cambridge:MIT Press,2001.
    [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.
    [13]McMillan KL.The SMV language.2001.http://www.cs.cmu.edu/~modelcheck/smv.html [1]范玉顺.工作流管理技术基础.北京:清华大学出版社,2001.5-22.
    [2]李慧芳,范玉顺.工作流系统时间管理.软件学报,2002,13(8):1552-1558.http://www.jos.org.cn/1000-9825/13/1552.pdf
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

王远,范玉顺.工作流时序约束模型分析与验证方法.软件学报,2007,18(9):2153-2161

复制
分享
文章指标
  • 点击次数:4165
  • 下载次数: 5788
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2006-03-28
  • 最后修改日期:2006-08-16
文章二维码
您是第19987962位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号