Modeling Recursive Search Algorithms by Means of Hierarchical Colored Petri Nets and CPN Tools

Author(s):  
Clarimundo Machado Moraes Junior ◽  
Rita Maria Silva Julia ◽  
Stephane Julia
Author(s):  
Шахла Сурхай Гусейнзаде

Статья посвящена моделированию нечеткого управления на сетях Петри (СП). Ставится задача разработки модели управления на СП с нечеткой логикой по информации, выраженной в лингвистической форме. На основе критериев работы водяного насоса в зависимости от изменяющего водопотребления определены всевозможные ситуации и события в системе. Для описания не полных знаний по поведению системы использованы лингвистические переменные «расход воды» и «скорость насоса». Термы этих переменных соответствуют их нечетким значениям и обозначаются выражениями, характеризующими одно из состояний системы. Фаззификация лингвистических переменных выполнена в среде Fuzzy Toolbox системы моделирования MATLAB. Описывая необходимое поведение системы отношениями между ситуациями и событиями с применением логики «Если... То...» разработана система правил управления насосного агрегата. Всевозможными ситуациями, событиями и отношениями между ними соответственно формированы множества позиций, переходов и дуг СП. Учитывая систему продукционных правил управления и структурных элементов СП, разработан алгоритм управления насосного агрегата. На основе разработанного алгоритма управления определены функции входных и выходных инциденций переходов в виде таблиц. Таблицы определяют матриц входных и выходных инциденций переходов. Разработана граф-модель СП. Модель описывает работу одного насосного агрегата. Визуализация модели реализована в системе CPN Tools (Colored Petri Nets Tools). Значения термов принимаются как атрибуты цветов раскрашенной сети Петри (РСП) и с применением CPN ML (Colored Petri Nets Markup Language) присваивается маркерам сети. С помощью значений термов описывается поведение и желаемая реакция системы. Проведены симуляционные эксперименты соответственно ситуациям в системе и анализ модели на основе свойств СП.


2021 ◽  
Author(s):  
Matheus Dias Gama ◽  
Stéphane Julia ◽  
Rita Maria Silva Julia

Frequentemente, a complexidade da política de distribuição dos algoritmos distribuídos os tornam extremamente hostis a consagradas abordagens matemáticas de análise de desempenho, tais como análise assintótica, técnicas de recorrências e análise probabilística. Isso se deve ao fato de que tais métodos não provêm recursos adequados que lhes permitam avaliar o quão o gradual aumento do número de processadores impacta no tempo de execução do algoritmo. Diante disso, este artigo propõe uma abordagem visual e formal, baseada em simulações automáticas de modelos de Redes de Petri Coloridas Hierárquicas no ambiente gráfico Colored Petri Nets Tools (CPN Tools), para avaliar o speedup e o ponto de saturação de processadores de algoritmos distribuídos usados em Inteligência Artificial. Será usado como estudo de caso o algoritmo de treinamento dos Perceptrons de Múltiplas Camadas baseado na retro-propagação do erro.


Author(s):  
Dmitry A. Zaitsev ◽  
Tatiana R. Shmeleva

Aviation and aerospace systems are complex and concurrent and require special tools for their specification, verification, and performance evaluation. The tool in demand should be easily integrated into the standard loop of model-driven development. Colored Petri nets represent a combination of a Petri net graph and a functional programming language ML that makes it powerful and convenient tool for specification of real-life system and solving both tasks: correctness proof i.e. verification and performance evaluation. This chapter studies basic and advanced features of CPN Tools – a powerful modeling system which uses graphical language of colored Petri nets. Starting with a concept of colored hierarhical timed Petri net, it goes through declaration of color sets and functions to peculiarities of hierarchical design of complex models and specification of timed characteristics. The authors accomplish the chapter with a real-life case study of performance evaluation for switched Ethernet network.


Information ◽  
2021 ◽  
Vol 12 (7) ◽  
pp. 277
Author(s):  
Anant Sujatanagarjuna ◽  
Arne Bochem ◽  
Benjamin Leiding

Protocol flaws such as the well-known Heartbleed bug, security and privacy issues or incomplete specifications, in general, pose risks to the direct users of a protocol and further stakeholders. Formal methods, such as Colored Petri Nets (CPNs), facilitate the design, development, analysis and verification of new protocols; the detection of flaws; and the mitigation of identified security risks. BlockVoke is a blockchain-based scheme that decentralizes certificate revocations, allows certificate owners and certificate authorities to revoke certificates and rapidly distributes revocation information. CPNs in particular are well-suited to formalize blockchain-based protocols—thus, in this work, we formalize the BlockVoke protocol using CPNs, resulting in a verifiable CPN model and a formal specification of the protocol. We utilize an agent-oriented modeling (AOM) methodology to create goal models and corresponding behavior interface models of BlockVoke. Subsequently, protocols semantics are defined, and the CPN models are derived and implemented using CPN Tools. Moreover, a full state-space analysis of the resulting CPN model is performed to derive relevant model properties of the protocol. The result is a complete and correct formal BlockVoke specification used to guide future implementations and security assessments.


Author(s):  
Dmitry A. Zaitsev ◽  
Tatiana R. Shmeleva

Aviation and aerospace systems are complex and concurrent and require special tools for their specification, verification, and performance evaluation. The tool in demand should be easily integrated into the standard loop of model-driven development. Colored Petri nets represent a combination of a Petri net graph and a functional programming language ML that makes it powerful and convenient tool for specification of real-life system and solving both tasks: correctness proof i.e. verification and performance evaluation. This chapter studies basic and advanced features of CPN Tools – a powerful modeling system which uses graphical language of colored Petri nets. Starting with a concept of colored hierarhical timed Petri net, it goes through declaration of color sets and functions to peculiarities of hierarchical design of complex models and specification of timed characteristics. The authors accomplish the chapter with a real-life case study of performance evaluation for switched Ethernet network.


Author(s):  
Sh. S. Huseynzade

A modification of the Petri nets is proposed  a Fuzzy Colored Petri Net (FCPN), leading to the integration of Fuzzy Petri Nets (FPN) and Colored Petri Nets (CPN). Separately, the shortcomings of FPN and CPN and the advantages the developed FCPN for modeling intelligent control systems are identified and justified. In the developed modified FCPN the membership functions of the terms of a linguistic variable are applied to markers of the CPN as color and fuzzy existence conditions are assigned to arcs depending on the values of the linguistic variable. As a result, FCPN with enhanced capabilities was obtained, which eliminates the shortcomings of CPN and FPN. The FCPN and a simulation approach are defined, which includes a reasoning algorithm, as well as a detailed procedure for modeling and analysis of nonlinear discrete objects. The structure is organized in the CPN Tools system with the synchronization of the CPN ML (Markup Language) language with the MatLab package. The choice of membership function and fuzzification of term values is performed in the Fuzzy Toolbox application of the MatLab system. The proposed approach is illustrated by simple example, including the control of water pumps, to maintain the required water level in the pumping well. A model is developed for the automation of adaptive fuzzy control of water pumps based on modified FCPN. Based on the criteria for the operation of water pumps according to the water levels in the pumping well, many positions and transitions of the FCPN are formed. Describing the necessary behavior of the system by the relations between the positions and transitions of the FCPN using the logic “If ... Then ...” an adaptation algorithm is developed. Based on the algorithm, the matrices of input and output incidents are determined. The graph model of the FCPN is developed. Visualization of the model is implemented in the CPN Tools system. The computer simulations and net analysis experiments demonstrate the convenience of the developed approach when modeling the intelligent control of dynamic systems.


2015 ◽  
Vol 19 (5) ◽  
pp. 115-130
Author(s):  
L. W. Dworza´nski ◽  
I. A. Lomazova

Nested Petri nets (NP-nets) are an extension of Petri net formalism within the “netswithin-nets” approach, when tokens in a marking are Petri nets, which have an autonomous behavior and are synchronized with the system net. The formalism of NP-nets allows modeling multi-level multi-agent systems with dynamic structure in a natural way. Currently, there is no tool for supporting NP-nets simulation and analysis. The paper proposes the translation of NP-nets into Colored Petri nets and the use of CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.


2020 ◽  
Vol 8 (1) ◽  
pp. 17-49 ◽  
Author(s):  
Said Meghzili ◽  
Allaoua Chaoui ◽  
Martin Strecker ◽  
Elhillali Kerkouche

The correctness of transformations has recently begun to attract the attention of the researchers in Model Driven Engineering (MDE). The objective of this article is twofold. First, it presents an approach for transforming BPMN models to Colored Petri nets models using GROOVE and EMF/Xpand tools. Second, it proposes an approach for checking the correctness of the transformation itself. More precisely, we have defined the termination property of the transformation and the preservation of some structural properties of BPMN models by the transformation using the GROOVE graph transformation tool. The authors have also applied the approach on a case study through which the authors have verified the successful termination of the transformation using GROOVE Model Checker and the target model properties using CPN Tools.


2014 ◽  
Vol 35 (11) ◽  
pp. 2608-2614
Author(s):  
Xiang Gao ◽  
Yue-fei Zhu ◽  
Sheng-li Liu

Sign in / Sign up

Export Citation Format

Share Document