共查询到18条相似文献,搜索用时 62 毫秒
1.
工作流过程建模方法及模型的形式化验证 总被引:1,自引:1,他引:1
Work/low technology is widely used in business process modeling, software process modeling as well as en-terprise information integration. At present, there exist a variety of workflow modeling approaches, which differ in the easiness of modeling, expressiveness and formalism. In this paper, the modeling approaches most used in research project and workflow products are compared. And the verification of workflow model is also dealt. We argue that a ideal workflow modelin~ approach is a hybrid one, i.e. the inteuration of the above approaches. 相似文献
2.
3.
4.
5.
工作流过程建模中的形式化验证技术 总被引:22,自引:2,他引:20
工作流过程建模是一个复杂且易错的过程.若过程定义在投入运行之后被发现有错,则修复错误的代价相当高,这个问题引起了研究界和工业界的高度重视.因此,在建模阶段进行有效的过程验证是十分必要的.综述了工作流过程验证技术的发展现状,包括强调验证的重要性,叙述了需要验证的问题和复杂度;介绍了对验证方法的要求;讨论了过程合理性验证和化简验证技术等;并通过对研究现状的分析和对比,提出了仍然没有解决的问题和将来的工作. 相似文献
6.
实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。 相似文献
7.
工作流过程建模是一个复杂且易错的过程,在建模阶段进行有效的过程验证是十分必要的。目前,柔性工作流验证领域的研究还比较欠缺,该文在这方面作了一些探索。把过程合理化验证和化简验证技术应用于基于交互学习的柔性工作流建模的形式化验证中,叙述了需要验证的问题和复杂度。利用Petri网的形式化基础特性对过程进行合理性验证和规约验证。根据规约粒度的不同,分别对基于交互学习的柔性工作流模型进行原子级和组件级规约。规约使用的基本技术有库所融合、变迁融合和子网融合。在特性保持的前提下,将过程模型缩小到适当规模。结果表明,基于交互学习的柔性工作流过程建模中的形式化验证方法具有一定的实用性和可操作性。 相似文献
8.
并发程序验证的时序Petri网方法 总被引:10,自引:0,他引:10
并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。 相似文献
9.
语义Web服务组合的形式化描述与验证研究 总被引:1,自引:0,他引:1
Web服务组合是Web服务的主要研究方向之一,对语义Web服务组合进行形式化描述并进行分析和验证是组合服务正确运行的保证.本文首先给出了基于有色Petri网的语义Web服务形式化模型,形式化描述了OWL-S的ServiceModel中8种基本的Web服务组合模式,利用这些组合模式可以构造出满足需求的组合Web服务.然后,对服务组合形式化模型的正确性分析和验证进行研究后,给出了组合模型语法正确性、可达性、活性和有界性的算法.最后,通过一个具体的建模实例展示了Web服务组合的Petri网建模. 相似文献
10.
基于Petri网的审计工作流模型设计与验证 总被引:1,自引:0,他引:1
针对计算机审计工作,结合工作流和Petri网方法,建立了一套审计工作流模型.引入了化简的验证方法,并通过化简,对模型进行了正确性验证.利用Petri网的方法,可以降低实际进行计算机审计工作的难度,为审计软件的开发提供了很好的支持. 相似文献
11.
BPMN(Business Process Modeling Notation)作为一个在系统开发早期阶段获取业务过程模型的标准,指导系统的设计和开发,其模型的正确性是影响软件开发质量的关键。鉴于BPMN模型的形式化可以验证模型的正确性,提出了一种利用扩展Petri网模型,应用模型驱动技术实现BPMN模型形式化自动执行的方法。该方法通过细化Petri网模型中的Transition和Place元素以及增加Organization Identifier和Group Identifier容器,使其不但能够描述BPMN模型中的动态行为,而且还能描述BPMN模型中的动态行为协作和静态组织结构。从元模型结构、语法和图标记方面详细分析了扩展的Petri网模型元素,利用模型驱动开发技术设计BPMN模型元素至扩展的Petri网模型元素的转换规则,并在Eclipse平台上使用ATL模型转换语言执行映射,实现形式化的自动执行。最后在此基础上应用Travel Agency系统演示了模型形式化插件BPMN2ExtendPetrinets的执行结果。 相似文献
12.
Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state
space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings—themselves
a class of acyclic Petri nets—which contain enough information, albeit implicit, to reason about the reachable markings of
the original Petri nets. In [19], a verification technique for net unfoldings was proposed, in which deadlock detection was reduced to a mixed integer linear
programming problem. In this paper, we present a further development of this approach. The essence of the proposed modifications
is to transfer the information about causality and conflicts between the events involved in an unfolding, into a relationship
between the corresponding integer variables in the system of linear constraints. Moreover, we present some problem-specific
optimisation rules, reducing the search space. To solve other verification problems, such as mutual exclusion or marking reachability
and coverability, we adopt Contejean and Devie's algorithm for solving systems of linear constraints over the natural numbers
domain and refine it, by taking advantage of the specific properties of systems of linear constraints to be solved.
Another contribution of this paper is a method of re-formulating some problems specified in terms of Petri nets as problems
defined for their unfoldings. Using this method, we obtain a memory efficient translation of a deadlock detection problem
for a safe Petri net into an LP problem. We also propose an on-the-fly deadlock detection method.
Experimental results demonstrate that the resulting algorithms can achieve significant speedups.
相似文献
Maciej KoutnyEmail: |
13.
14.
Ekkart Kindler Wolfgang Reisig Hagen Völzer Rolf Walter 《Formal Aspects of Computing》1997,9(4):409-424
A technique to model and to verify distributed algorithms is suggested. This technique (based on Petri nets) reduces the modelling and analysis effort to a reasonable level. The paper outlines the technique using the example of a typical network algorithm, theecho algorithm.Supported by the DFG-projects Verteilte Algorithmen and Konsensalgorithmen 相似文献
15.
16.
17.
基于Petri网的工作流结构正确性化简验证方法 总被引:2,自引:0,他引:2
工作流技术是近年来在计算机应用领域发展最为迅速的新技术之一,但基于覆盖图的工作流网的结构正确性检查的实现过于复杂.本文在Aalst提出的基于Petri网的工作流网的控制流的正确性理论的基础上,提出了工作流网的正确性检查的化简规则及相应的化简算法,实现了对于正确结构的工作流网直接验证;对于错误结构的工作流网,输出其包含问题节点在内的子网结构,可以进一步通过覆盖图的方法确认问题节点,从而降低了工作流网正确性检查的复杂性. 相似文献
18.
模式进化是工作流管理系统的一个主要特点之一.以缺乏正确性分析的工作流模式进化为例,指出进化后的模式会存在着数据流冲突或控制流结构错误,并以Aalst提出的工作流网的建模方法为形式化描述,对工作流管理系统中增加变迁的工作流模式进化进行了分析,提出了无数据流冲突的模式进化算法,及进化时保证控制流结构正确性的进化插入规则,并给出了相关的正确性验证, 相似文献