工作流过程建模方法及模型的形式化验证

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.     

不可否认协议的Petri网建模与分析

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用．作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们．以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质．使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷．     

基于受控计时扩展Petri网的分拣系统建模

分拣系统中 ,由于操作人员的参与 ,可能导致被分拣货物和装箱清单不一致。这主要是由于上包控制和货包信息的同步跟踪不可控所造成。为解决这个问题 ,该文提出受控计时扩展Petri网 ,在此基础上对自动分拣系统进行了建模 ,并分析了操作人员的控制作用。实际应用表明 ,受控计时扩展Petri网为具有人参与的物流系统提供了一种良好的建模方法。     

模糊有色Petri网的形式化推理算法研究

Petri网以其图形化的表示方式广泛应用于形式化推理中.基于模糊有色Petri网的形式化推理算法,以系统内部事务之间的逻辑关系为依据,充分利用模糊Petri网在分析不确定知识中的优势,通过知识模糊、库所抽象、转换抽象实现层次化的知识表示和知识推理,并结合有色Petri网对系统规模作适当约简,从而构造出了一种新型的模糊着色网(FCPN)知识表示和获取模型,有效弥补了传统Petri网在实际应用中的缺陷,使模糊推理过程更加简单且易于实现.     

基于Colored Petri网的工作流建模及应用

对传统Petri网在描述工作流模型时,组成模型的元素数量过多、无法体现数据流以及无法管理多个工作流实例等缺陷,将有色Petri网（Colored Petri net,CPN）理论的分析方法引入到工作流网（Workflow-net,WF-net）,实现二者有机结合,提出了一种新型扩展工作流网CPWF-net（Workflow-net based on Colored Petri net）,给出了严格的定义,使能机制和触发,全面分析了CPWF-net的特性,并就其实际应用进行了初步探究。     

基于扩展Petri网模型的BPMN形式化

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的执行结果。     

基于Petri网的混合安全策略建模与验证

提出了一种基于有色Petri网的建模方法,在系统的Petri网模型中可以对中国墙策略进行分析和验证.给出了基于有色Petri网的混合安全策略的形式化定义;并通过一个系统实例阐述了如何利用该方法对系统的混合安全性进行分析和验证.无论是在系统的设计阶段还是实现阶段,该方法都能够有效地提升系统的混合安全性.     

基于Petri网的协议并行化处理模型的描述和验证

本文提出了一个ＯＳＩ／ＲＭ运输层协议并行处理模型，以适应协议的高效处理，根据模型特点，使用Ｐｅｔｒｉ网作为形式化描述工具，对该模型进行描述，分析和验证。     

基于Petri网的UML形式化建模应用分析

UML是功能强大的图形化建模语言,但存在缺乏精确的语义描述的特点,因此UML形式化研究一直是一个热点.Petri网既有直观的图形表示,又有坚实的数学基础,拥有许多成熟的分析方法可以直接用于分析模型的性能.结合一个图录编纂应用系统,使用基于Petri网的建模方法,对该系统的UML状态图和序列图进行了形式化分析.排除UML模型中的缺陷,在软件设计阶段发现错误,降低软件开发的花销,最终达到提高了软件的质量的目的.     

基于Petri网的UML形式化建模应用分析

UML是功能强大的图形化建模语言,但存在缺乏精确的语义描述的特点,因此UML形式化研究一直是一个热点。Petri网既有直观的图形表示,又有坚实的数学基础,拥有许多成熟的分析方法可以直接用于分析模型的性能。结合一个图录编纂应用系统,使用基于Petri网的建模方法,对该系统的UML状态图和序列图进行了形式化分析。排除UML模型中的缺陷,在软件设计阶段发现错误,降低软件开发的花销,最终达到提高了软件的质量的目的。     

密码协议验证中的Petri网方法

如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确.利用Petri网给出了一种用于密码协议验证的形式化方法.在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型.最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题.证明了这种方法的有效性.     

基于Petri网的工作流合法性验证综述

对传统的工作流合理性验证方法进行了阐述,并分析了这些方法的优缺点,着重针对国内外学者用Pe-tri网对工作流合理性验证方法进行综述,分析其特点,并指出了工作流的合理性验证的发展方向。     

一种基于有色Petri网的安全协议分析方法研究

利用有色Petri网建模工具CPN tools中的查询函数对安全属性进行描述,搭建一个能够覆盖大部分安全性质的CPN查询函数库,提出一种基于CPN的通用和规范的安全协议形式化分析语言,该语言可以像用面向对象编程语言编程一样对安全协议进行建模。     

Modeling and formal verification of embedded systems based on a Petri net representation

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.     

基于Petri网的实时多智能体系统建模

给出基于Petri网的实时多Agent系统建模方法,它通过Petri网建立由接口模块、目标模块、计划模块、调度模块、知识库模块、环境模块、内部模块和控制模块组成的实时Agent模型,抽象和清晰地描述出实时Agent内部和外部特征。     

基于有色Petri网的SPIN协议建模与分析

在无线传感器网络路由协议的研究中,对现有协议的分析和验证具有重要意义.形式化建模是分析验证网络协议的一种有效方法.使用形式化工具有色Petri网对无线传感器网络中的SPIN路由协议进行形式化描述,并使用CPN Tools分析和验证了该协议的活性、可达性、有界性等特性.     

基于Petri网的单向PWM整流电路建模

PWM整流电路是交-直-交变流器的重要电路,是包括连续和离散事件的混杂系统,具有并发、异步等特点。Petri网是描述和分析异步并发现象的一种有效的混杂系统建模工具。本文以Petri网为工具,从一个全新角度,建立单相PWM整流电路的模型,对其电路特性进行了分析。     

基于模糊Petri网的瓦斯突出空间模型

瓦斯突出相关影响因素具有明显的时空特性,煤层突出危险程度的判别是一个多因素决定的模糊事件,模糊Petri网在离散事件动态建模具有突出的优势。在分析瓦斯突出空间数据分布及模糊性应用基础上,对比分析基本Petri网和模糊Petri网的知识表示,结合瓦斯突出各因素空间分布的特点,扩展了模糊Petrie网的相关组件成分,建立基于模糊Petri网的瓦斯突出空间模型,使瓦斯突出影响因素在不同的空间位置通过空间模型表示出来,进一步描述了瓦斯突出空间位置动态转换,在实际预测中具有现实的意义和可操作性。     

一种扩展了价格信息的着色Petri网及其应用

基于实际业务流程建模中成本预算分析的需要，在着色网的基础上扩展了价格信息，提出了价格着色网。讨论了价格着色网的变迁规则，并以一个业务流程实例介绍了价格着色网的分析技术及其应用，实验结果表明着色网扩展价格信息是可行的而且是有效的。