Modularization, Composition, and Hierarchization of Petri Nets with Heraklit
几十年来，人们都知道，如果没有模块化和分解的概念，就无法理解基于计算机的系统。我们提出了一个普遍的，富有表现力的，直观的吸引力的组合操作的Petri网，结合细化的概念和代数表示的网及其组成。案例研究表明，大型系统可以由微小的网络片段组成。在未来，需要更多的实地研究，以更好地了解所提出的想法在现实世界中的后果。
2022-02-03 cs.SE
Automated Test Case Generation using Petri Nets
软件测试是确定软件系统的精度、质量、完整性和安全性的过程。软件测试的一个重要步骤是测试用例的生成，测试用例的质量对测试的时间和成本起着至关重要的作用。在这项研究中，它表明，结构和行为图可以用来表示规格在一个单一的模型，使用高级Petri网（HLPN）。本文研究了基于Petri网的测试模型自动生成问题。此外，从非形式化模型（UML）生成一致的形式化模型（HLPN）是本研究的重点。
2015-09-28 cs.SE
Timed Test Case Generation Using Labeled Prioritized Time Petri Nets
软件和硬件系统的基于模型的测试使用系统的行为和形式模型。提出了一种基于模型的实时系统黑盒一致性测试技术，采用标记优先时间Petri网（LPrTPN）。定时输入/输出关联（tioco）关系，它考虑到环境假设，作为参考，以确定实现的正确性。测试套件是从LPrTPN自动派生的，LPrTPN由两个并发子网组成，分别指定被测系统及其环境。在测试用例具有最短可能的执行累积时间的意义上，结果是最优的。测试用例选择结合了测试目的和与模型相关的结构覆盖标准。在SE-LTL公式中规定了测试目的或覆盖标准。扩展了TINA Petri网分析器，使其支持并发组合Petri网.使用Tina工具箱自动生成时间最优的测试套件，结合了模型检查器selt和路径分析器计划。selt输出满足逻辑公式的序列。计划计算这个序列的最快执行，它将在测试用例套件中转换。
2012-06-04 cs.SE
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-10 cs.SE
Web Services Modeling and Composition Approach using Object-Oriented Petri Nets
如今，随着电子商务等新技术的出现和发展，大量的公司连接到Internet，并提出了Web服务来进行交易。所提出的Web服务是概念上受限于相对简单功能的组件。一般来说，单一的服务已经不能满足越来越复杂的用户需求。因此，必须使服务能够组合以提供增值服务。提出了一种基于面向对象Petri网的Web服务组合方法。在他的上下文中，表达代数，成功地解决了Web服务的复杂组合问题，提出了。一个Java工具，允许自动化这种方法，基于一个明确的代数和G-网元模型，我们提出的，开发。
2013-04-08 cs.SE
Lending Petri nets and contracts
基于编排的服务组合方法通常假设，在找到一组正确扮演编排所规定角色的服务之后，每个服务都尊重自己的角色。诚实的服务不受对手的保护。我们提出了一个模型的合同的基础上扩展的Petri网，它允许服务，以保护自己，同时仍然实现编排。我们将此模型与命题合同逻辑，通过显示翻译到我们的Petri网的公式，保留了逻辑概念的协议，并允许组合验证。
2013-05-30 cs.LO cs.MA cs.SE
Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems
本文提出了一种多Agent系统事件日志与嵌套Petri网之间的组合一致性检验方法。通过将事件日志投影到模型组件上，可以在每个投影的日志和相应的组件之间执行一致性检查。我们正式证明了我们方法的有效性，证明检查嵌套Petri网的适应度等效于检查其每个组件的适应度。利用嵌套Petri网的多代理系统结构，该方法可以为每个系统组件提供特定的一致性诊断，以及避免在分解模型进行一致性检查时计算人工边界。
2020-03-16 cs.LO cs.MA cs.SE
Translating UML State Machines to Coloured Petri Nets Using Acceleo: A Report
UML状态机被广泛用于指定动态系统行为。然而，它的语义描述是非形式化的，从而阻碍了模型检验技术的应用，可以保证系统的安全性。在以前的工作中，我们提出了一个形式化的非并发UML状态机使用有色Petri网，以便允许形式化验证。在本文中，我们报告了我们的经验，实现这种翻译的自动化方式使用模型到文本转换工具Acceleo。虽然Acceleo提供了有趣的功能，促进了我们的翻译过程，但它也有难以克服的局限性。
2014-05-06 cs.LO cs.SE
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-04 cs.DC cs.ET cs.SE
Compositional model checking of concurrent systems, with Petri nets
组合性和进程等价性都是进程代数的标准概念。复合性意味着一个复合系统的行为只依赖于其组成部分的行为，即没有涌现行为。过程等价意味着系统的显式状态空间让位于其交互模式：环境可以通过交互获得的信息。Petri网是一个经典的，但被广泛使用和理解的并发模型。然而，它们经常被描述为非组合模型，并且工具倾向于处理整体的、全局指定的模型。本教程论文集中在Petri网与边界（PNB）：1-安全网的合成，图形代数，以及其应用程序中的可达性检查工具彭罗斯。该算法的特点是使用组合性和进程等价，一个强大的组合，可以利用，以提高性能的检查可达性和覆盖性在几个常见的例子，其中Petri网模型现实的并发系统。
2016-03-03 cs.FL cs.LO cs.SE
Constructing Coverability Graphs for Time Basic Petri Nets
基于时间的Petri网是一种用于实时系统建模的强大形式主义，其中时间约束通过与转换相关联的标记的时间描述的时间函数来表示，表示可能的触发时间。我们介绍了一种基于有限图的可覆盖性分析技术。该技术进一步利用时间匿名概念[5，6]，为了处理拓扑无界网，利用TA令牌覆盖的概念，即，一种ω匿名时间戳这样的覆盖性分析技术是能够构建覆盖性树/图无界的时间基本Petri网模型。只要在输入模型中，可以匿名化无限制增长的令牌，就可以保证算法的终止。这意味着我们能够管理不表现出Zeno行为的模型，并且不表达依赖于无限过去事件的行为。这实际上是一个合理的限制，因为通常情况下，真实世界的示例不会表现出这种行为。
2014-09-19 cs.LO cs.SE
A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems
Petri网（PN）是一个中心的，理论上健全的并发或分布式系统的模型，但至少在其经典的定义，没有表达不够，以表示动态重构能力。另一方面，重写逻辑已被证明是并发/分布式系统的几个形式化模型的自然语义框架。我们提出了一个紧凑，高效的莫德形式化的动态可重构PT网（抑制剂弧），作为一个运行的例子，一个简单的，容错的制造系统的规范。我们讨论了这样一个组合的方法的优点，以及它引起的一些问题。
2021-11-16 cs.LO cs.SC cs.SE
Coordination Level Modeling and Analysis of Parallel Programs using Petri Nets
在过去的十五年中，高性能计算（HPC）社区已经要求并行编程环境，其调和分布式存储器并行计算平台的通用性、更高抽象级别、可移植性和效率。哈希组件模型似乎是解决HPC社区要求满足这些要求的替代方案。本文提出的基础，将使一个基于哈希模型的并行程序设计环境，以解决问题的“调试”，性能评估和验证的形式属性的并行程序通过一个强大的，简单的，广泛采用的形式主义：Petri网。
2012-08-19 cs.DC cs.PL cs.SE
Discovering Object-Centric Petri Nets
RWTH Aachen University（亚琛工业大学）；Fraunhofer Institute for Applied Information Technology（弗劳恩霍夫应用信息技术研究所）
从事件数据中发现Petri网的技术假设每个事件只有一个案例标识符。这些案例标识符被用来关联事件，由此发现的Petri网旨在描述单个案例的生命周期。事实上，并不存在一个可能的案例概念，而是多个相互交织的案例概念。例如，事件可以指订单、项目、包、客户和产品的混合。一个包可以指多个物品、多个产品、一个订单和一个客户。因此，我们需要假设每个事件都引用一个对象集合，每个对象都有一个类型（而不是一个case标识符）。这种以对象为中心的事件日志更接近于现实生活中的信息系统中的数据。从一个以对象为中心的事件日志，我们要发现一个以对象为中心的Petri网的地方，对应于对象类型和转换，可以消费和生产不同类型的对象的集合。以对象为中心的Petri网可视化了不同类型对象之间的复杂关系。本文讨论了一种新的进程发现方法在PM4Py中实现。正如将要证明的那样，如果需要的话，发现可以用于向下钻取到特定视点的整体过程模型确实是可行的。
2020-10-05 cs.AI cs.FL cs.LG
