arXiv 1209.23822012-09-08cs.SE

2012年Petri Nets模型检验竞赛的原始报告

Raw Report on the Model Checking Contest at Petri Nets 2012

F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, L. Fronc, L. M. Hillah, N. Lohmann, E. Paviot-Adet, F Pommereau, C. Rohr, Y. Thierry-Mieg, H. Wimmel, K. Wolf

备注：: 78 pages

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文介绍了在2012年在汉堡举行的Petri Nets上举行的模型检验竞赛的结果。本次竞赛旨在对应用于Petri网的模型检验技术的性能进行公平和实验性的评估。这是继2011年成功举办之后的第二届。参与的工具进行了比较几个考试（状态空间生成和几种类型的公式-结构，可达性，LTL，CTL的评价）上运行的一组常见的模型（地点/过渡和对称Petri网）。在对比赛进行了简短的概述之后，本文提供了来自上下文、每个模型的模型和每个考试的考试的原始结果。

英文摘要：

This article presents the results of the Model Checking Contest held at Petri Nets 2012 in Hambourg. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the second edition after a successful one in 2011. The participating tools were compared on several examinations (state space generation and evaluation of several types of formulae - structural, reachability, LTL, CTL) run on a set of common models (Place/Transition and Symmetric Petri nets). After a short overview of the contest, this paper provides the raw results from the context, model per model and examination per examination.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Petri网模型检验竞赛2013年报告

Model Checking Contest @ Petri Nets, Report on the 2013 edition

本文档介绍了在米兰Petri Nets 2013上举行的模型检验竞赛的结果。本次竞赛旨在对应用于Petri网的模型检验技术的性能进行公平和实验性的评估。这是继2011年和2012年两次成功举办后的第三届。参与的工具进行了比较几个考试（状态空间生成和评价几种类型的formula-reachability，LTL，CTL的各种类别的原子命题）上运行的一组常见的模型（地点/过渡和对称Petri网）。在对比赛进行了简短的概述之后，本文提供了比赛的原始结果，每个模型的模型和每个考试的考试。还提供了本报告的HTML版本（http：mcc.lip6.fr）。

2013-09-10cs.SE

Petri网和流动事物的机器

Petri Nets and Machines of Things That Flow

Petri网是一种用于建模和分析系统行为的成熟的图形形式主义。Petri网的价值的一个重要考虑因素是它们在描述建模形式主义的语法和语义方面的使用。用形式化技术（如Petri网）描述建模符号提供了一种最小化模糊性的方法。因此，必须对Petri网有深入而多样的理解。本文是针对一个新的，但初步的，探索这样一个重要的工具的语义。具体来说，本文关注的是与Petri网的语义解释的建模语言的基础上的概念，机器的东西流。从事物流的角度分析了几种Petri网图的语义。结果表明，该方法用于探索Petri网的基本假设是可行的。

2018-08-29cs.SE

Petri网的基本要素

Essentials of Petri nets

本文重点介绍了Petri网中常被忽视但作者认为重要或有趣的概念与方面，特别是Carl Adam Petri所强调的内容。

2024-08-27cs.SE

用UML-RSDS求解Petri网到状态图的转换

Solving the Petri-Nets to Statecharts Transformation Case with UML-RSDS

本文提供了一个解决方案的Petri网状态图的情况下，使用UML-RSDS。我们展示了如何使用这种方法可以给出一个高度声明性的解决方案，这是融合和可逆的。

2013-12-02cs.SE

着色Petri网的态射

Morphisms of Coloured Petri Nets

我们引入了色网之间的态射的概念。我们的定义一般Petris定义为普通网。有色网的态射映射了底层无向网的拓扑空间以及关联映射的核和上核。核是沿着态射的转移边界纤维的流，上核是位置边界纤维的标记类。绑定，颜色，流和标记类的子网的附件形式化的使用层理论的概念。有色网是Petri空间上的层-上层对，有色网之间的态射是这样的对之间的态射。有色网和它们的态射形成一个范畴。我们证明了一类关于类的态射的子范畴中乘积的存在性。在引入标记后，我们的概念推广到有色Petri网。

2006-08-07cs.SE

用FunnyQT解决Petri-Nets到Statecharts转换案例

Solving the Petri-Nets to Statecharts Transformation Case with FunnyQT

FunnyQT是一个用于函数式Lisp方言Clojure的模型查询和模型转换库，提供了丰富而高效的查询和转换API。本文描述了TTC 2013 Petri-Nets到Statcharts转换案例的FunnyQT解决方案。该解决方案获得了该案例的最佳整体解决方案奖和最佳效率奖。

2013-12-02cs.SE

更多相关论文收起更多论文

用Heraklit实现Petri网的模块化、组合和层次化

Modularization, Composition, and Hierarchization of Petri Nets with Heraklit

几十年来，人们都知道，如果没有模块化和分解的概念，就无法理解基于计算机的系统。我们提出了一个普遍的，富有表现力的，直观的吸引力的组合操作的Petri网，结合细化的概念和代数表示的网及其组成。案例研究表明，大型系统可以由微小的网络片段组成。在未来，需要更多的实地研究，以更好地了解所提出的想法在现实世界中的后果。

2022-02-03cs.SE

基于Petri网的测试用例自动生成

Automated Test Case Generation using Petri Nets

软件测试是确定软件系统的精度、质量、完整性和安全性的过程。软件测试的一个重要步骤是测试用例的生成，测试用例的质量对测试的时间和成本起着至关重要的作用。在这项研究中，它表明，结构和行为图可以用来表示规格在一个单一的模型，使用高级Petri网（HLPN）。本文研究了基于Petri网的测试模型自动生成问题。此外，从非形式化模型（UML）生成一致的形式化模型（HLPN）是本研究的重点。

2015-09-28cs.SE

基于面向对象Petri网的Web服务建模与组合方法

Web Services Modeling and Composition Approach using Object-Oriented Petri Nets

如今，随着电子商务等新技术的出现和发展，大量的公司连接到Internet，并提出了Web服务来进行交易。所提出的Web服务是概念上受限于相对简单功能的组件。一般来说，单一的服务已经不能满足越来越复杂的用户需求。因此，必须使服务能够组合以提供增值服务。提出了一种基于面向对象Petri网的Web服务组合方法。在他的上下文中，表达代数，成功地解决了Web服务的复杂组合问题，提出了。一个Java工具，允许自动化这种方法，基于一个明确的代数和G-网元模型，我们提出的，开发。

2013-04-08cs.SE

时序图测试用例描述及基于时间弧Petri网的虚拟集成分析

Sequence Diagram Test Case Specification and Virtual Integration Analysis using Timed-Arc Petri Nets

在本文中，我们正式定义测试用例序列图（TCSD）作为一个易于使用的手段来指定测试用例的组件，包括时间约束。这些测试用例是使用UML2语法建模的，并且可以由标准的UML建模工具指定。在基于组件的设计中，可以在实际系统构建之前通过组件的虚拟集成来实现对错误的早期识别。我们定义了这样一个过程，它集成了各个组件的测试用例，根据给定的体系结构的互连和检查，如果所有指定的通信序列是一致的。因此，我们正式定义的转换TCSD到时间弧Petri网和这些网的组合过程。我们的方法的适用性，证明了航空电子用例从ARP 4761标准。

2013-02-21cs.SE

借贷Petri网与契约

Lending Petri nets and contracts

基于编排的服务组合方法通常假设，在找到一组正确扮演编排所规定角色的服务之后，每个服务都尊重自己的角色。诚实的服务不受对手的保护。我们提出了一个模型的合同的基础上扩展的Petri网，它允许服务，以保护自己，同时仍然实现编排。我们将此模型与命题合同逻辑，通过显示翻译到我们的Petri网的公式，保留了逻辑概念的协议，并允许组合验证。

2013-05-30cs.LOcs.MAcs.SE

嵌套Petri网的组合一致性检验与多Agent系统的事件调度

Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems

本文提出了一种多Agent系统事件日志与嵌套Petri网之间的组合一致性检验方法。通过将事件日志投影到模型组件上，可以在每个投影的日志和相应的组件之间执行一致性检查。我们正式证明了我们方法的有效性，证明检查嵌套Petri网的适应度等效于检查其每个组件的适应度。利用嵌套Petri网的多代理系统结构，该方法可以为每个系统组件提供特定的一致性诊断，以及避免在分解模型进行一致性检查时计算人工边界。

2020-03-16cs.LOcs.MAcs.SE

用Acceleo实现UML状态机到有色Petri网的转换

Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report

UML状态机被广泛用于指定动态系统行为。然而，它的语义描述是非形式化的，从而阻碍了模型检验技术的应用，可以保证系统的安全性。在以前的工作中，我们提出了一个形式化的非并发UML状态机使用有色Petri网，以便允许形式化验证。在本文中，我们报告了我们的经验，实现这种翻译的自动化方式使用模型到文本转换工具Acceleo。虽然Acceleo提供了有趣的功能，促进了我们的翻译过程，但它也有难以克服的局限性。

2014-05-06cs.LOcs.SE

如何将量子烘焙到你的宠物Petri网中并拥有你的网络理论

How to Bake Quantum into Your Pet Petri Nets and Have Your Net Theory Too

RMIT University（皇家墨尔本理工大学）

Petri网已经在许多应用领域中得到了广泛的使用，尤其是由于其基于偏序依赖和并发执行的用于交互的分布式和异步过程和服务的组合的人性化图形语法。Petri网还具有抽象语义，以及用于组合合成，结构检查和行为分析的数学方法。这些导致了对实时、分布式和并行程序设计语言、软件和服务系统使用各种网络，以考虑它们的接口和交互协议。这些启示使得Petri网对于专注于组件、组件之间的相互依赖和面向环境的交互的分布式软件架构方法非常宝贵。量子计算--特别是量子软件工程--正处于起步阶段，可以从软件体系结构研究和网络理论、方法及其应用的积累中受益。在本文中，我们建立了Petri网和量子系统之间的联系，使网的理论和组件体系结构可能有助于综合和分析抽象的软件模型和它们的接口协议的混合经典和量子程序设计语言和服务系统。我们利用网络形式主义的一些见解，为软件规范的一个多功能的食谱烤量子到现存的Petri网的味道，并证明量子编程的Petri网的普遍性和组合性。

2021-06-04cs.DCcs.ETcs.SE

并发系统的组合模型检验，用Petri网

Compositional model checking of concurrent systems, with Petri nets

组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。

2016-03-03cs.FLcs.LOcs.SE

时间基本Petri网覆盖图的构造

Constructing Coverability Graphs for Time Basic Petri Nets

基于时间的Petri网是一种用于实时系统建模的强大形式主义，其中时间约束通过与转换相关联的标记的时间描述的时间函数来表示，表示可能的触发时间。我们介绍了一种基于有限图的可覆盖性分析技术。该技术进一步利用时间匿名概念[5，6]，为了处理拓扑无界网，利用TA令牌覆盖的概念，即，一种ω匿名时间戳这样的覆盖性分析技术是能够构建覆盖性树/图无界的时间基本Petri网模型。只要在输入模型中，可以匿名化无限制增长的令牌，就可以保证算法的终止。这意味着我们能够管理不表现出Zeno行为的模型，并且不表达依赖于无限过去事件的行为。这实际上是一个合理的限制，因为通常情况下，真实世界的示例不会表现出这种行为。

2014-09-19cs.LOcs.SE

动态可重构系统的一种可行模型--可重写Petri网的Maude实现

A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems

Petri网（PN）是一个中心的，理论上健全的并发或分布式系统的模型，但至少在其经典的定义，没有表达不够，以表示动态重构能力。另一方面，重写逻辑已被证明是并发/分布式系统的几个形式化模型的自然语义框架。我们提出了一个紧凑，高效的莫德形式化的动态可重构PT网（抑制剂弧），作为一个运行的例子，一个简单的，容错的制造系统的规范。我们讨论了这样一个组合的方法的优点，以及它引起的一些问题。

2021-11-16cs.LOcs.SCcs.SE

基于Petri网的并行程序协调级建模与分析

Coordination Level Modeling and Analysis of Parallel Programs using Petri Nets

在过去的十五年中，高性能计算（HPC）社区已经要求并行编程环境，其调和分布式存储器并行计算平台的通用性、更高抽象级别、可移植性和效率。哈希组件模型似乎是解决HPC社区要求满足这些要求的替代方案。本文提出的基础，将使一个基于哈希模型的并行程序设计环境，以解决问题的“调试”，性能评估和验证的形式属性的并行程序通过一个强大的，简单的，广泛采用的形式主义：Petri网。

2012-08-19cs.DCcs.PLcs.SE

发现对象中心Petri网

Discovering Object-Centric Petri Nets

RWTH Aachen University（亚琛工业大学）；Fraunhofer Institute for Applied Information Technology（弗劳恩霍夫应用信息技术研究所）

从事件数据中发现Petri网的技术假设每个事件只有一个案例标识符。这些案例标识符被用来关联事件，由此发现的Petri网旨在描述单个案例的生命周期。事实上，并不存在一个可能的案例概念，而是多个相互交织的案例概念。例如，事件可以指订单、项目、包、客户和产品的混合。一个包可以指多个物品、多个产品、一个订单和一个客户。因此，我们需要假设每个事件都引用一个对象集合，每个对象都有一个类型（而不是一个case标识符）。这种以对象为中心的事件日志更接近于现实生活中的信息系统中的数据。从一个以对象为中心的事件日志，我们要发现一个以对象为中心的Petri网的地方，对应于对象类型和转换，可以消费和生产不同类型的对象的集合。以对象为中心的Petri网可视化了不同类型对象之间的复杂关系。本文讨论了一种新的进程发现方法在PM4Py中实现。正如将要证明的那样，如果需要的话，发现可以用于向下钻取到特定视点的整体过程模型确实是可行的。

2020-10-05cs.AIcs.FLcs.LG