Modeling and analysis of responsive space launch system based on timed colored Petri NeT

Responsive space launch is currently developing rapidly and has application cases in many fields, with advantages such as fast response speed and flexible networking. Aiming at the efficiency evaluation of responsive space launch system, this article first summarizes the typical process of fast space launch, and then gives a hierarchical model of a space fast launch system based on timed colored Petri nets, including top-level model, demand model, command decision model, launch Model, measurement and control model, and finally use CPN Tools to simulate and verify the model, analyze the basic characteristics of the model and the performance of the system, and provide data support and theoretical basis for the optimization of the fast space launch system.

Speedup Evaluation of the Training Algorithm for a Multilayer Perceptron based on Colored Petri Nets Simulations

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.

Formal Security Evaluation and Improvement of Wireless HART Protocol in Industrial Wireless Network

With the rapid development of wireless communication technology in the field of industrial control systems, Wireless HART is an international wireless standard, because of its low cost and strong scalability, as well as its wide range of applications in the industrial control field. However, it is more open communication so that the possibility of increased attacks by external. At present, there are many types of research on wireless protocol security at home and abroad, but they all focus on the realization of the security function of the protocol itself, which has certain limitations for the formal modeling of the protocol security assessment. Taking into account the aforementioned research status, this paper takes the Wireless HART protocol as the research object and adopts the model detection method combining eCK model theory and colored Petri net theory to evaluate and improve the security of the protocol. First, the colored Petri net theory and CPN Tools modeling tool were introduced to verify the consistency of the original model of the protocol. And the eCK model was used to evaluate the security of the original protocol model. It was found that the protocol has two types of man-in-the-middle attack vulnerabilities: tampering and deception. Aiming at the attack loopholes of the protocol, an improvement plan was proposed. After improving the original protocol, CPN Tools modeling tool was used for security verification. It was found that the new scheme improvement can effectively prevent the existing attacks and reasonably improve the security of the protocol.

Formalizing the Blockchain-Based BlockVoke Protocol for Fast Certificate Revocation Using Colored Petri Nets

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.

Event logs gerados da simulação de diferentes cenários e analisados com mineração de processos.

A cada dia uma quantidade enorme de dados é gerada de sistemas gerenciados por informações. Geralmente esta informação é armazenada em banco de dados ou event logs. Mineração de processos pode utilizar esta informação para prover conhecimento útil para empresas. O objetivo deste trabalho é produzir event logs de diferentes cenários de simulação e analisá-los utilizando mineração de processos. Estes cenários tentam simular atividades contidianas em um ambiente de escritório. Um exemplo é o cenário de recurso fuzzy que tenta simular a incerteza inerente em atividades realizas por humanos. Para alcançar este objetivo algumas ferramentas open-source foram utilizadas. CPN Tools foi utilizada para construir e simular a Workflow net baseada na rede “Handle Complaint Process” e gerar os event logs durante as simulações. ProM foi utilizado para aplicar os algoritmos de process discovery e conformance checking nos event logs gerados. O algoritmo utilizado foi o Inductive Visual Miner. A comparação entre os cenários mostrou uma diferença significativa entre os tempos de execução devido ao propósito de cada cenário. Com este tipo de simulação de cenários, donos de negócios podem realizar simulações de possíveis cenários de sua empresa e estimar melhores deadlines para seus clientes.

Modeling and Analysis of Network Control System Based on Hierarchical Coloured Petri Net and Markov Chain

This paper investigates a modified modeling of networked control systems (NCSs) with programmable logic controller (PLC). First, the controller-to-actuator and sensor-to-controller network-induced delays are investigated by a modeling tactics based on hierarchical coloured petri net (HCPN) in a structure-conserving way. Comparing with the recent result, the signal transmission delay is set in a random interval instead of a fixed mode; moreover, the data packet drop out and disorder are also taken into consideration. Second, delays captured form CPN tools are analyzed with a strategy based on Baum–Welch algorithm and statistics science. Besides, time delays are modeled as a Markov chain and the transition probabilities is calculated using the consequent from the previous operation. Finally, a comparison verification illustrates the equivalence property between proposed models.

Overload Control in a Token Player for a Fuzzy Workflow Management System

The underlying proposal of this work is to control overload of a Token Player in a Fuzzy Workflow Management System. In order to accomplish this, possibility theory is used to measure how much the Token Player can be overloaded. The model used in this work is built using Colored Petri net and the simulation is made using CPN Tools. Finally, is possible to control overload of the Token Player in a Fuzzy Workflow Management System, nevertheless more time is spent to achieve the end of activities.

Modeling With Colored Petri Nets

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.

A Method for Modeling and Simulation of Lossy Queuing System

Queuing is a common phenomenon in daily life. The theory of queuing provides theoretical basis and optimization scheme for queuing in real life. However, due to the limitation of time and space, the queuing problem in real life is not an ideal queuing model, and the field verification of the queuing model with losses consumes a lot of manpower, material resources and financial resources. In this paper, a queuing model with loss mechanism was established by using color Petri net. One-dimensional random walk model was improved and introduced into the queuing system to further reveal the principle of loss in queuing. CPN tools were used to simulate the model. By comparing the experimental results with the actual results, the correctness of the model is proved, which fully indicates that the model can well explain the loss of queuing system in real life.