计算机科学 ›› 2007, Vol. 34 ›› Issue (11): 118-123.

• • 上一篇    下一篇

基于时态逻辑的工作流分析

  

  • 出版日期:2018-11-16 发布日期:2018-11-16
  • 基金资助:
    国家自然科学基金助项目(No.60573046).

  • Online:2018-11-16 Published:2018-11-16

摘要: 工作流的属性规约语言需要具有高表达力以及基于状态和事件的推理能力。本文提出了一种时态逻辑规约语言E-CTL^*,该语言集成了状态和事件,能够精确和直觉地表示验证的属性。工作流的畅通性验证无论在时间上还是空间上代价都是非常高的,状态空间爆炸是验证的主要困难所在。利用E-CTL^*描述畅通性,可以使用存在的符号化模型检测工具验证畅通性,在一定程度上克服了状态爆炸问题。同时模型检测技术给出失效路径的优点可以引导我们纠正工作流的错误。工作流的变动需要具有正确性。从时态逻辑的角度讨论了变动正确性问题,得出了保持变动

关键词: 工作流 时态逻辑 过程变动 同步网

Abstract: Specification languages for workflow need to combine practical algorithmic efficiency with high expressive power and the ability to reason about both states and events. We address this question by defining a new temporal logic E-CTL^* which integrates bot

Key words: Workflow, Temporal logic, Process change, Synchronization net

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!