共查询到20条相似文献,搜索用时 156 毫秒
1.
构件交互风格和交互协议的描述与验证是基于构件的分布式系统开发的基础和关键,而构件交互协议是一种典型的分布式并发系统.传统的方法难以解决系统建模和验证中的所谓的状态爆炸问题.偏序简化是应用迹的概念,对模型进行化简并且对模型进行死锁验证.但这样的验证重点放在了Petri网模型上,而没有涉及进程代数模型,所验证的只是模型是否有死锁状态.而以通信系统演算CCS为代表的进程代数,因其概念简洁,可用的数学工具丰富,在分布式并发系统的规范、分析、设计和验证方面获得了广泛应用.对此,提出将偏序规约应用于进程代数模型,给出基于进程代数模型的偏序简化算法,并提出利用进程代数模型偏序简化算法来验证安全性的方法. 相似文献
2.
基于Petri网化简技术的工作流过程模型结构验证 总被引:2,自引:1,他引:1
目前,工作流系统向大型化发展,这使得基于可达图的验证技术在对大型模型进行验证时面临着状态空间爆炸的问题.因此,在过程验证之前,对大型模型进行化简是必要的.文中介绍两种化简规则.这些规则将一个大的Petri网化简为更小的Petri网,同时保持合理性属性,保证化简后的Petfi网和原有的Petri网具有相同的属性.介绍了Petri网、Workflow Petri网和过程合理性定义;讨论了针对Petri网的两种化简技术;提出了工作流过程模型结构合理性验证过程. 相似文献
3.
4.
5.
为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK的模型检测问题转换为无实时算子的PBTLK的模型检测问题;其次,定义PBTLK的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小. 相似文献
6.
7.
8.
基于Petri网的信息流安全属性的分析与验证* 总被引:2,自引:0,他引:2
信息流安全属性的定义均基于不同的语义模型,很难作出比较,以Petri网作为描述安全系统的统一模型,在Petri网上定义四种常见的安全属性,并分析它们之间的逻辑关系。在信息流安全属性验证方面,传统的方法称为展开方法,该方法适用于确定型系统,而对于非确定型系统,该方法是可靠的,但不完备。进一步对Petri网上已经定义的四种属性给出可靠完备的验证算法,并开发出相应的验证工具。最后通过实例说明了验证方法在搜索隐通道方面的应用。 相似文献
9.
着色Petri网模型检测工具的扩展及其在Web服务组合中的应用 总被引:1,自引:0,他引:1
Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模型检测工具--CPN Tools--中使用ML(meta language)语言实现了这些算法,然后将扩展后的CPN模型检测工具应用在Web服务组合的验证问题中.该方法不仅可以验证Web服务组合是否存在逻辑错误,还能告诉用户发生错误的原因,为Web服务组合的验证提供了技术上的保障.实验表明对着色Petri网的模型检测工具的扩展是正确、有效的. 相似文献
10.
Petri网的符号ZBDD可达树分析技术 总被引:2,自引:0,他引:2
Petri网是一种适合于并发系统建模、分析和控制的图形工具.可达树是Petri网分析的典型技术之一,它通过标识向量集合表征系统的状态空间,组合复杂性严重制约了该分析技术可处理系统问题的规模.零压缩决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)是一种新型的数据结构,是表示和处理稀疏向量集合的一种有效技术.文章基于Petri网町达标识向量的稀疏特征,给出了Petri网分析的符号ZBDD技术,该技术通过对标识向量(状态)的布尔向量表示、可达标识向最(状态)的符号ZBDD生成,实现Petri网可达状态空间的高效符号操作和紧凑符号表示.实验表明,基于ZBDD的符号可达性分析算法能够有效处理较大规模Petri网问题. 相似文献
11.
基于Petri网与SimEvents的半导体晶圆生产线建模与仿真 总被引:1,自引:0,他引:1
SimEvents与Petri网相结合是一种很好的复杂生产线建模仿真方法,应用这一方法建立了一条300mm晶圆生产线的仿真模型.描述了其Petri网模型建立的总体流程和各个详细步骤,以及在SimEvents环境下实现Petri网模型并进行仿真的关键技术.在此基础上,对晶圆生产的不同调度方案分别进行了仿真,并把仿真结果进行了比较,从而验证了仿真建模方法的正确性. 相似文献
12.
We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL. 相似文献
13.
João Pascoal Faria Ana C. R. Paiva 《International Journal on Software Tools for Technology Transfer (STTT)》2016,18(3):285-304
Novel techniques and a toolset are presented for automatically testing the conformance of software implementations against partial behavioral models constituted by a set of parameterized UML sequence diagrams, describing both external interactions with users or client applications and internal interactions between objects in the system. Test code is automatically generated from the sequence diagrams and executed on the implementation under test, and test results and coverage information are presented back visually in the model. A runtime test library handles internal interaction checking, test stubs, and user interaction testing, taking advantage of aspect-oriented programming techniques. Incremental conformance checking is achieved by first translating sequence diagrams to Extended Petri Nets that combine the characteristics of Colored Petri Nets and Event-Driven Petri Nets. 相似文献
14.
Coloured Petri Nets (CPNs) are a graphically oriented modelling language for concurrent systems based on Petri Nets and the functional programming language Standard ML. Petri Nets provide the primitives for modelling concurrency and synchronisation. Standard ML provides the primitives for modelling data manipulation and for creating compact and parameterisable CPN models.Functional programming and Standard ML have played a major role in the development of CPNs and the CPN computer tools supporting modelling, simulation, verification, and performance analysis of concurrent systems. At the modelling language level, Standard ML has extended Petri Nets with the practical expressiveness required for modelling systems of the size and complexity found in typical industrial projects. At the implementation level, Standard ML has been used to implement the formal semantics of CPNs that provide the theoretical foundation of the CPN computer tools.This paper provides an overview of how functional programming and Standard ML are applied in the CPN modelling language and the supporting computer tools. We give a detailed presentation of the key algorithms and techniques used for implementing the formal semantics of CPNs, and we survey a number of case studies where CPNs have been used for the design and analysis of systems. We also demonstrate how the use of a Standard ML programming environment has allowed Petri Nets to be used for the implementation of systems. 相似文献
15.
基于有色Petri网的经营过程建模 总被引:18,自引:0,他引:18
在经营过程重组(BPR)的过程中,利用仿真工
具对经营过程建模与仿真分析,被认为是快速和顺利实施BPR的必要手段.目前大多数BPR支
持工具局限于对过程的仿真,而Petri网则因其严格的数学定义和丰富的分析方法,不仅能
够仿真过程的性能参数,还可以对过程的结构进行分析,从而在过程诊断和重组方案的设计
中发挥重要作用.将有色Petri网应用于经营过程建模,可以较好地描述经营过程的不确定
性、并发性和资源共享等问题,并解决模型中存在的冲突、死锁等问题,同时避免了普通Pe
tri网过于复杂的缺点. 相似文献
16.
Yuanzhuo Wang Chuang Lin Peter D. Ungsunan Xiaomeng Huang 《The Journal of supercomputing》2011,56(1):79-105
In this paper, we propose a service composition model method that supports quantitative computation based on Stochastic Petri
Nets (SPN). It can capture the semantics of complex service combinations and their respective specifications. In this method,
services are divided into interior services and exterior services. The exterior services will be published to the users, while
the interior ones do not need to be published. Six equivalent simplified theorems which can be used to simplify the complex
models of interior services to simple models of exterior services are presented. They enable the minimization of the state
space of the model and make quantitative computation feasible. In addition, since Grid services are always affected by all
kinds of churns in actual applications, we also research survivability and its main attributes for Grid service composition.
The definition and computational methods based on the model are put forward. In the end, we use the method presented above
to describe and analyze an example of travel Grid services successfully. 相似文献
17.
基于非马尔可夫随机Petri网的软件再生建模与分析 总被引:2,自引:0,他引:2
软件老化是影响软件系统可靠性的重要潜在因素,软件再生作为一种主动预防性的软件容错技术是解决软件老化问题的主要手段.以往的随机Petri网再生模型假定所有变迁的实施时间服从指数分布.针对变迁的实施时间服从确定性分布或一般性分布的情况,文中提出了一种用非马尔可夫随机Petri网建立软件再生模型的方法.该方法采用马尔可夫再生理论对模型进行分析,并给出模型的瞬态解和稳态解.仿真实验表明:选择合适的软件再生周期,可以有效地降低存在老化的软件系统的平均宕机成本,提高系统的可用性和可靠性. 相似文献
18.
19.
《Theoretical computer science》2005,346(1):58-95
The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate for analyzing timing properties of concurrent systems by model checking. However, even if very compact state representations are obtained thanks to the use of constraints in tccp, large state spaces can still be generated, which may prevent model-checking tools from verifying tccp programs completely. Model checking tccp programs is a difficult task due to the subtleties of the underlying operational semantics, which combines constraints, concurrency, non-determinism and time. Currently, there is no practical model-checking tool that is applicable to tccp. In this work, we introduce an abstract methodology which is based on over- and under-approximating tccp models and which mitigates the state explosion problem that is common to traditional model-checking algorithms. We ascertain the conditions for the correctness of the abstract technique and show that this preliminary abstract semantics does not correctly simulate the suspension behavior, which is a key feature of tccp. Then, we present a refined abstract semantics which correctly models suspension. Finally, we complete our methodology by approximating the temporal properties that must be verified. 相似文献
20.
本文首先将模拟技术应用于Petri网中,得到模糊Petri网模型,然后基于Petri网中的库所湾量的概念,在普通Petri网的反馈控制基础上提出了一种模型Petri网的反馈控制方法。该方法使得对复杂系统的模糊Petri多控制器的系统设计成为可能。 相似文献