Search

The article is devoted to fuzzy control modelling based on Petri nets (PN). The aim of the study was to develop a Petri net-based control model with fuzzy logic for information expressed in a linguistic form. The criteria of the water pump’s operation, depending on the changing water consumption, were used to determine various situations and events in the system. Linguistic variables such as “water flow rate” and “pump speed” were used to describe incomplete knowledge about the system’s behaviour. The terms of these variables correspond to their fuzzy values and are denoted with expressions characterizing one of the system’s states. The fuzzification of linguistic variables was implemented in the Fuzzy Toolbox environment of the MATLAB modelling system. A system of rules for the pump unit’s control was developed by means of describing the required behaviour of the system by the relationship between situations and events using the logic «If ... Then ...». All sorts of situations, events, and relations between them formed sets of PN positions, transitions, and arcs. An algorithm for the control of the pump unit was developed with the consideration of the system of the production rules of control and PN structural elements. Based on the developed control algorithm, the functions of the input and output transition incidents were defined and shown in tables. The tables define the matrices of the input and output transition incidents. The PN graph model was developed. The model describes the operation of one pump unit. The visualization of the model was implemented in the CPN Tools system (Coloured Petri Nets Tools). The values of the terms are taken as attributes of the colours of the coloured Petri net (CPN) and by using CPN ML (Coloured Petri Nets Tools Markup Language) are assigned to the network markers. The values of the terms were used to describe the behaviour and the desired reaction of the system. Simulation experiments referring to the system’s situations and model analysis were carried out.

Smart contracts increasingly cause attention for its ability to widen blockchain's application scope. However, the security of contracts is vital to its wide deployment. In this article, we propose a multilevel smart contract modeling solution to analyze the security of contract. We improve the program logic rules for bytecode and apply the Hoare condition to create a Colored Petri Net (CPN) model. The model detection method provided by the CPN tools can show the full-state space and the wrong execution path, which help us analyze the security of the contract from several perspectives. The example shows that the counter-example path given by the contract model is accord with our expected results based on code analysis, proving the correctness of the solution. In addition, we design a highly automated modeling method, introducing custom call libraries and a path derivation algorithm based on backtracking, which improves the efficiency and pertinence of the dynamic simulation of CPN models.

Video games are complex systems that combine technical and artistic processes. The specification of this type of system is not a trivial task, making it necessary to use diagrams and charts to visually specify sets of requirements. Therefore, the underlying proposal of this work is to present an approach based on the formalism of Petri nets for aiding in the design process of video games. The activities of the game are represented by a specific type of Petri net called WorkFlow net. The definition of a topological map can be represented by state graphs. Using Colored Petri nets, it is possible to define formal communication mechanisms between the model of activity and the model of the map. The simulation of the timed models allows then to produce an estimated time that corresponds to the effective duration a player will need to complete a level of a game. Furthermore, a kind of Soundness property related to gameplay in a game Quest can be verified through state space analysis. For a better understanding of the approach, the video game Silent Hill II is used.

[1] SZI «Strazh NT». Rukovodstvo administratora. URL: http://www.guardnt.ru/download/doc/admin_guide_nt_3_0.pdf (accessed: 25.05.2019) (in Russian). [2] Sistema zashchity informacii ot nesankcionirovannogo dostupa «Strazh NT». Opisanie primeneniya. URL: http://www.rubinteh.ru/public/opis30.pdf (accessed: 25.05.2019) (in Russian). [3] Popov A.D. Modeli i algoritmy ocenki effektivnosti sistem zashchity informacii ot nesankcionirovannogo dostupa s uchyotom ih vremennyh harakteristik v avtomatizirovannyh sistemah organov vnutrennih del: dis kand. tekhn. nauk. Voronezh / 2018. URL: https://vi.mvd.rf/Nauka/Dissovety/sostojavshiesja_zashhiti_dissertacij (accessed: 25.05.2019) (in Russian). [4] Ventcel' E.S. Teoriya veroyatnostej. – М.: Nauka, 1969. – 576 s. (in Russian). [5] Jensen K. and Kristensen L.M. Coloured Petri Nets Modeling and Validation of Concurrent Systems. Berlin: Springer-Verlag 2009. [6] Sinegubov S.V. Modelirovanie sistem i setej telekommunikacij. Voronezh: VI MVD RF, 2016. – 336 s. (in Russian). [7] Zaitsev D.A., Shmeleva T.R. Simulating Telecommunication Systems with CPN Tools: Students' book. – Odessa: ONAT, 2006. – 60 p. [8] Grigor'ev V.A., Karpov A.V. Imitacionnaya model' sistemy zashchity informacii. Programmnye produkty i sistemy. Tver': MNIIPU i NII «Centrprogrammsistem», 2005. №2. S. 26–30 (in Russian). [9] Piterson D.ZH. Teoriya setej Petri i modelirovanie sistem: Per. s angl. – M.: Mir, 1984. – 264 s. (in Russia). [10] Kotov V.E. Seti Petri. Moskva: Nauka. Glavnaya redakciya fiziko-matematicheskoj literatury, 1984. – 160 s. (in Russian). [11] Drovnikova I.G., Zmeev A.A., Popov A.D., Rogozin E.A. Methodology for investigating the probability-time characteristics of network attacks in the simulation modelling software environment. Herald of dagestan state technical university. Technical sciences. 2017. 44 (4). P. 99–113. DOI: https://doi.org/10.21822/2073-6185-2017-44-4-99-113 (in Russian). [12] Meedeniya D. A. Indika Perera Model based software design: Tool support for scripting in immersive environments. IEEE 8th International Conference on Industrial and Information Systems, 2013. P. 248–253. [13] Lukaszewski R., Winiecki W. Petri Nets in Measuring Systems Design. IEEE Instrumentation and Measurement Technology Conference Proceedings, 2006. P. 1564–1569. [14] Gehlot V., Nigro C. An introduction to systems modeling and simulation with Colored Petri Nets. 2010. P 104–118. [15] Shang Guan Wei [et. al.] Research of System Modeling and Verification Method Combine with UML Formalization Analysis and Colored Petri Net Third International Symposium on Intelligent Information Technology Application, 2009. P. 488–491.

Complex Event Processing (CEP) is an event-based technology that allows us to process and correlate large data streams in order to promptly detect meaningful events or situations and respond to them appropriately. CEP implementations rely on the so-called Event Processing Languages (EPLs), which are used to implement the specific event types and event patterns to be detected for a particular application domain. To spare domain experts this implementation, the MEdit4CEP approach provides them with a graphical modeling editor for CEP domain, event pattern and action definition. From these graphical models, the editor automatically generates a corresponding Esper EPL code. Nevertheless, the generated code is syntactically but not semantically validated. To address this problem, MEdit4CEP is extended in this paper by Prioritized Colored Petri Net (PCPN) formalism, resulting in the MEdit4CEP-CPN approach. This approach provides both a novel PCPN domain-specific modeling language and a graphical editor. By using model transformations, event pattern models can be automatically transformed into PCPN models, and then into the corresponding PCPN code executable by CPN Tools. In addition, by using PCPNs we can compare the expected output with the actual output and can even conduct a quantitative analysis of the scenarios of interest. To illustrate our approach, we have conducted an air quality level detection case study and we show how this novel approach facilitates the modeling, simulation, analysis and semantic validation of complex event-based systems.

Petri net is a mathematical tool for concurrent systems. This paper suggests colored Petri net to model basic operations of quantum algorithm. We construct a colored Petri net model of Grover's algorithm using CPN Tools. Simulation is done to show usefulness of the proposed model.

The tracing system of agricultural products plays a role in guaranteeing their quality and safety. It has multiple modules to accomplish traceability. Its reliability is the premise to ensure the normal operation of the tracing system. Because the modules of the system run concurrently with each other, the unverified system cannot guarantee the rationality of the design for the relationship among the modules, such as the hierarchy of the system modules and the concurrent coupling of the modules when the system runs, which is one of the reasons leading to the reliability problem of the system. Color Petri net is a kind of improved Petri net tools. This paper analyzes the operation of the modules of agricultural product traceability system. It uses colored Petri net of agricultural products tracing system for modeling, and uses the hierarchical petri net to design the method of reducing the size of the model to ensuring that the system module design of the border. with a color set represents the transmission of information between different modules. Finally, CPN Tools are used to verify the model. The results shows that this model detection method can ensure the reliability of the tracing system of agricultural products.

Process mining can be understood as a tool to extract useful information from processes that already happened and make decisions to improve performance of processes. The main three techniques while applying process mining to event logs are process discovery, process enhancement and conformance checking. Among many different applications that process mining can be applied to, in this paper, process mining is used to discover the model from event logs generated from simulations of the "Handle Complaint Process" Workflow net based on a p-time Petri net model with hybrid resources. This net discovered with process mining must be similar to the original one due event logs used to generate it are created from the simulation. There is no doubt that process mining has become increasingly useful for the future of Workflow nets especially when it is followed by simulation. Process mining can discover processes from event logs, find deviations and produce a better workflow while simulation can test new scenarios and hypotheses. With both working together product owners can reach a pretty good process excellence. The "Handle Complaint Process" Workflow net based on a p-time Petri net model with hybrid resources tries to solve the real time scheduling problem of Workflow Management Systems. The approach made in this work in particular, utilizes discrete + continuous resources and real time to decide when to fire a transition in the Workflow net. To generate the event logs from the simulation of the Workflow net, some functions were added in order to capture the identification number of each token, the path made by it, as well as the timestamp in the moment the transition was fired and the person or system responsible for the activity. This Workflow net was simulated using CPN Tools. The logs generated from the simulation were converted using the ProM Import tool and the process mining discovery technique was applied using ProM. The use of event logs of a business process model is a way to detect deviations from the expected behavior. Based on these deviations, the process can be changed in order to achieve excellence. The logs from the p-net model with hybrid resources tries to simulate, in a better way, the human behavior. As the model generated from the logs is similar to the original one, the conversion is correct. As a future work proposal, we will compare a real event log with the results achieved with this work to see the efficiency in simulating a process model with hybrid resources.

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.

With the increasing availability of robots and image processing systems, the automated robotic line implementations are still extensively increasing. As well, the complexity of these systems increases, which increases the demands on the determination of their function and possible analysis. For these purposes the complex robotic systems are modeled. Here, the Coloured Petri Nets were used to model the robotic sorting line. Specifically, the CPN Tools software was used to model creation, simulation, analysis and to made experiments. State space analysis was done to revelation of possible unwanted deadlocks. Furthermore, the sorting line model was used to found out the maximum number of objects that can be sorted in a defined time. As the robot manipulation time directly affects maximum number of objects in one batch, the timing procedure was created to declare robot operation dependency on types of manipulated object. The state space analysis showed that there are no unwanted deadlocks in the system. The model has been verified and declared as correct. Optimal composition and order of objects was successfully found by timed coloured Petri nets experiments.

This article examines the issues of modeling a forecasting agent based on extensions of Petri nets. For this, a new class of Petri nets, fuzzy-neural Petri nets, was developed. It made it possible to build a model for predicting a change in the situation from standard to boundary and abnormal. The implementation of this model in the CPN Tools software package is also considered.

This paper presents a Hierarchical Coloured Petri Nets model specifically designed to support the implementation process of a virtual workplace in Nigerian Universities. CPN Tools 4.0 was used to capture the various phases and activities of the framework for the implementation of a virtual workplace into a Hierarchical Coloured Petri Nets (CPN) model. The developed virtual workplace CPN model has been analyzed using simulation, and state space analysis methods. The developed CPN model being a graphical and also an executable representation of the implementation framework; will assist those empowered with the responsibility of implementing a virtual workplace to have a better understanding of the implementation process.

Recently, threats such as global warming and epidemics have become more serious. For chronic patients, it is desirable to evaluate the residual risks of telemedicine more accurately, including for combined hazards. However, such comprehensive evaluations are difficult to perform using existing risk assessment methods because telemedicine systems are distributed. To the best of our knowledge, existing research does not take the problem sufficiently into account. To assess the residual risk of telemedicine accurately, we study risk assessment using Coloured Petri Nets (CPN) for telemedicine, which is a formal modeling language that is well suited for modeling and analyzing complex systems. We evaluate the residual risks using simulation function by CPN Tools and obtain the residual risks more accurately. Given the results of an experiment we conduct using CPN for telemedicine, we can confirm the probability of not being able to consult telemedicine and other probabilities. Moreover, CPN is found to be well suited for assessing the combined hazards more accurately. This is the first paper of frequency probabilistic risk assessment using CPN for telemedicine.

The development of existing signal acquisition systems has long-term and high-cost problems. To deal with such situation, this paper takes the dust signal acquisition system as an example, and proposes a modeling method combining Information Flow Hierarchical Dynamic (IFHD) with Inhibitor arcs Hierarchical Coloured Petri Nets (IHCPN). The method first establishes a Unified Modeling Language (UML) model based on the functional block diagram of the system. To simplify the reference model, improved the transformation rules between the UML model and Petri Nets (PN) model. To ensure the validity, safety, and rationality of the reference model, the dynamic analysis of the constructed PN model is carried out by using the analysis method of the reachable marking graph. The simulation results of CPN Tools show that the model satisfies boundedness, reachability, liveness, and fairness, conforms to the performance indicators of system operation. Compared with the modeling method of Hierarchical Coloured Petri Nets (HCPN), IHCPN can greatly reduce the number of model nodes and connecting arcs, reduce the complexity of the system model, and provide a reliable reference model while effectively save system development time and cost.

In a multiplayer game scenario, the actions of a player most often have a direct influence on the actions of other players. Thus, the flow of the game can be changed causing an uncertainty behavior. This paper presents a method for modeling multiplayer video game scenarios based on a particular kind of Petri net, called WorkFlow net possibilistic. The constructors of the Possibility WorkFlow nets allow to represent the logical sequences of the actions of a game scenario, as well as the uncertainty behavior generated from the possible interactions between the players. The simulation of the model implemented in the CPN Tools tool allows to show through a gameplay graph the influence of the number of players in the effective participation of each player in the various activities proposed in the game. To illustrate the proposed approach, the game Tom Clancy's Ghost Recon: Wildlands is used.

This paper presents the model of intersection controllers using timed automata and colored Petri nets formalisms. The models include cars control, pedestrians control, vehicles detection system and failure diagnosis with subsequent control changes. The validation and verification of the models has been realized in UPPAAL Pro model-checker and CPN Tools. The proposed modeling framework is applied to real intersections located in Bratislava and Malacky, Slovakia.

Construction of Cyber-Physical Systems (CPS) by reusing or composing existing components (sub-systems) is the emerging need in software based system development. For software development, a number of paradigms exists to deal with the reusability at different levels. Component-based development (CBD) represents a paradigm shift in software development for its emphasis on development for/with reuse. Software composition mechanisms are the essence of this paradigm. In general, a software system in CBD is comprised of two kinds of elements: computation and communication. Defining/creating these elements in a generic way and for system construction allowing these elements to be customised in specific to the system needs can increase the level of reusability. In this paper, for a development paradigm (referred to as EX-MAN in CBD) for CPS construction, we focus on software elements dealing with the communications elements (referred to as connectors) among the computational elements. We define constraints (written in our proposed flow constraint language (FCL)) as a property for coordination by the exogenous connectors to customise the behaviour of connectors for system construction. In this paper, the semantics of FCL constraints for a sample exogenous connector is described for system construction/execution. In order to verify the operational semantics of FCL constraints of this exogenous connector, we use Coloured Petri Nets (in CPN tools) to model and simulate the connectors with constraints. Exogenous connectors are implemented in a tool exogenous composition framework (ECF) for system construction.

The paper presents development and verification methods and means of requirements and design solutions formal models. They are intended to create complex critical automated information systems in a same model-language and information-software environment for all its participants. The development and verification processes are carried out in an automated way on the basis of subject-oriented ontologies. Ontologies describe the quality management processes of software and hardware complexes at the stages of requirements justification and system design. They are developing by means modeling and design languages SysML, FUML, OCL structures and mechanisms, the Petri nets mathematical apparatus, time automata and time logics. In order to execute of validation and verification for complex of requirements and design solutions, construction and model execution route analysis algorithms in the VM FUML virtual machine environment are developed. Integration and use methods for specialized verification tools CPN Tools, Rodin, SPIN and Modelica as means to automated testing of complex requirements and design solutions models are proposed. This complex provides more effective interaction between the customer and the contractor both in the development of requirements and in the design of the system, along with this, detection and provides limination of defects through the automated verification, validation and correction procedures implementation. This approach application will improve the quality of requirements and design solutions, as well as improve economic performance by reducing the financial and time costs, which associated with the implementation of additional work in the case of defects, and when changing requirements or operating conditions.

Time and value throughputs reflect the actual workload and gross profit of enterprises over a period of time, respectively. Both of them are of great importance to the operation of data-aware workflow processes, since they can help managers to balance production capacity at each stage as well as determine how much capital should be recycled over a period of time. However, the existing methods have not investigated both time and value throughputs of data-aware workflow processes. In this paper, we propose a new approach to modeling and simulation of time and value throughputs of data-aware workflow processes. First of all, we construct an abstract model with time and value elements. Second, the abstract model is transformed into a simulation model in CPN Tools. Finally, we obtain and analyze the time and value throughputs automatically via the simulation logs. Compared with the existing methods, this is the first attempt to propose both time and value throughputs of data-aware workflow processes, and the whole procedure of modeling and simulation of them. Furthermore, the procedure of obtaining time and value throughputs through analyzing the logs is proposed, and a prototype system is designed and developed.

It is well known that formal verification of a large railway signalling system encounters the state explosion problem. To alleviate the problem, researchers usually concentrate on only route interlocking and abstract away other properties. Besides the route interlocking, there are also other vital properties to which failure to comply could potentially lead to danger. According to our experience, most of train accidents often involve human error and errors in other properties rather than errors in the route interlocking. Thus, we encounter a dilemma between fully automated validation of an incomplete model or partial validation of a complete model. We argue that formally modelling the complete model will be more valuable for the on-going projects of the State Railway of Thailand (SRT) because it provides insights and can be used to train new signal engineers. This paper focuses on the complete Coloured Petri Net model of a typical Thai railway signalling system: a double-line station with one passing loop. The model includes train movements that can be simulated and graphically visualized. According to SRT’s signalling principles, we have identified nine properties: route interlocking, alternative overlap, flank protection, aspect sequence, approach signal release, approach lock, back lock, sectional route release and quick route release. Lessons learnt from using CPN Tools to model and validate the railway signalling systems are also discussed.

We extend an approach to component allocation on heterogeneous embedded systems using Coloured Petri Nets (CPNs). We improve the CPN model for the embedded systems and outline a technique that exploits CPN Tools, a well-known CPN tool, to efficiently analyze embedded system's state space and find optimal allocations. The approach is model-based and represents an advancement towards a model-driven engineering view of the component allocation problem. We incorporate communication costs between components by extending the CPN formalism with a non-trivial technique to analyze the generated state space. We also suggest a technique to improve the state space generation time by using the branching options supported in CPN Tools. In the evaluation, we demonstrate that this technique significantly cuts down the size of the generated state space and thereby reduces the runtime of state space generation and thus the time to find an optimal allocation.

Congestion management capability is an important requirement for any quality of services (QoS) networking technology. Therefore, IEEE 802.1Qau has proceeded a congestion notification project whose aim is to develop a Carrier Ethernet congestion control scheme at Layer 2 for a data center network. A data center network should be efficient and robust to handle the growing demands of cloud computing. A congestion control scheme is a key component of data transport in this kind of network. The quantized congestion notification (QCN) scheme is a congestion management scheme, which has been standardized and designed to be implemented in the Carrier Ethernet. Coloured Petri net (CPN) is a modelling technique used with the Petri nets modelling tool. This technique is exploited to model and simulate the QCN in order to help understand the QCN scheme and derive performance measures. This paper proposes a formal model for the QCN scheme. Then, we verify the implementation of our model by simulations. Thus, the QCN queue and rate performances are evaluated using the CPN tools. Moreover, an improved model called TAI-QCN is proposed in order to enhance the QCN scheme.

High-level Petri nets such as Coloured Petri Nets (CPNs) are characterised by the combination of Petri nets and a high-level programming language. In the context of CPNs and CPN Tools, the inscriptions (e.g., arc expressions and guards) are specified using Standard ML (SML). The application of simulation and state space exploration (SSE) for validating CPN models traditionally focusses on behavioural properties related to net structure, i.e., places and transitions. This means that the net inscriptions are only implicitly validated, and the extent to which their sub-expressions have been covered is not made explicit. The contribution of this paper is an approach that establishes a link between coverage analysis known from programming languages and net inscriptions of CPN models. Specifically, we consider Modified Condition/Decision Coverage (MC/DC) of Boolean SML decisions, which cannot be measured within CPN Tools neither through state space exploration nor model checking directly. We have implemented our approach in a library for CPN Tools comprised of an annotation and instrumentation mechanism that transparently intercepts and collects evaluation of boolean conditions, and a post-processing tool that, for a set of model executions (runs), determines whether each decision is MC/DC-covered. We evaluate our approach on four large publicly available CPN models.

The using of digital logistics, based on intensive developments of smart technologies, into the system of product supply allows achieving optimal conditions for a certain period with the expected efficiency level. At the same time, it is necessary to consider increasing demand trend for these services in the sphere of agro-products supply from Ukraine to European Union markets. The use of “smart systems, “Internet of Things” (IoT), big data allows to quickly obtain info from hardware and other drives: technical tools installed on trucks, containers, ships, for operational monitoring and control of technological processes, as well as for making accurate forecasts. The presented supply system is distributive and parallel working with asynchronous interactions. Therefore, it is proposed to use the type of Petri nets - CPN tools to study systems behavior in enough depth and to obtain information about their most important characteristics. Models developed based on Petri nets have shown that in addition to clarity and simplicity in application, they allow considering various probabilistic factors. This fact allows us to simulate, analyze and predict works for all system participants according to promptly calculated values for each specific management object.

The article discusses issues related to the construction and implementation of search web services. Algebra for modeling and building web services is presented. As the basic operations for algebra are used: sequence, alternative selection and cycle. In addition, combined operations are determined based on the basic ones. The operations were chosen to provide a general and extended set of operations for the implementation of web search services. After defining each construction, the formal semantics of the operator is given in terms of Petri nets. An example of modeling and development of a real estate web-service in the CPN Tools. The indexes of efficiency of the developed service.

It is necessary for having the formal model of railway network in order to ensure the desirable behaviors of the rail transportation system. An alternative of formalizing the high-level railway network is proposed using hierarchical timed coloured Petri nets. The train stations and their interlink railways are concerned as the high-level building blocks to construct a specific railway network. The timed coloured Petri nets would be formally defined for a particular building block of the network hierarchically. The lower level modules construction and rules for making the hierarchical railway network model are provided. The resulting model is verified by using CPN tools to ensure the correctness, safety, and liveness.

Flowchart is a common graphical representation of a process or step-by-step solution for a problem simply drawn in the software design stage. A flowchart helps visualize how an algorithm works to solve a problem better than the program source code. However, it is crucial and beneficial to validate the correct behavior of the flowchart automatically using the formal methods. In this paper, we propose a scheme of transforming a basic flowchart into a coloured Petri net so that the designated model could be validated beforehand. A set of mapping rules is proposed to construct the resulting coloured Petri net from a given flowchart. The basic data types, including integer, boolean, and string, are coped in order to simulate the changing of state of variables in the flowchart. The resulting coloured Petri net are simulated and verified to ensure the correctness of its behavior using CPN tools.

Petri Net, a widely studied mathematical formalism, is a graphical notation for modeling systems. Petri Nets provide the foundation for modeling concurrency, communication, synchronization, and resource sharing constraints that are inherent to many systems. However, Petri Nets do not scale well when it comes to modeling and simulating large systems. Colored Petri Nets (CPNs) extend Petri Nets with a high level programming language, making them more suitable for modeling large systems. The CPN language allows the creation of models as a set of modules in a hierarchical manner and permits both timed and untimed models. Untimed models are used to validate the logical correctness of a system, whereas timed models are used to evaluate performance. This tutorial introduces the reader to the vocabulary and constructs of both Petri Nets and CPNs and illustrates the use of CPN Tools in creating and simulating models by means of familiar simple examples.

This paper presents an overview of several modeling methods, tools and approaches which are suitable for the network protocol design. In the beginning of the paper the necessity of the modeling usage during the protocol design is explained. Then Petri Nets features are summarized together with their basic definition and explanation on simple graphical model example. Later, Colored Petri Nets are presented with emphasis on differences from original Petri Nets and their features are explained on graphical representation of simple model created using CPN Tools. The paper is concluded with a brief explanation of modeling approaches most suitable for network protocol modeling.

Current formalized description is a key issue for semantic web services. Related works attempt at analyzing and verifying for web service composition with traditional Petri nets. However, Petri nets can only show the flow of process, in this paper we specify basic definitions of CPNs and 4 basic structures of web service described by CPN model. Finally, the author presented CPNs to model web service composition by CPN tools. The feasibility and effectiveness on the CPNs has been verified by simulation result.

The “SmartCity: Lagoa” project is a partnership within the “Portugal 2020” project, a municipality-scale installation of 20,000 IoT devices over the next 3 years. These devices include sensors for temperature, humidity, luminosity, volumetry, noise, carbon monoxide, pH, and ORP, among others; all transmitting the collected data to one of six gateways using LoRa technology. In the implementation of this project, a lack of tools allowing the simulation of LoRa based projects was detected. This paper presents a framework to simulate and monitor a project based on LoRa, using a precise and executable graphical language. The simulation can use, as input, real data from the implemented system and other data added for simulation purposes. This allows a basis on reality introducing useful information to guide the simulation to the intended tests. The behaviors are defined using CPN Tools, a design environment allowing editing, simulation, and verification of high-level Petri net models. This paper presents the system design and how the executable models are used to simulate and validate the model, namely the system behavior when gateways and sensors are connected and disconnected.

Online shopping systems integrating multiple participants have rapidly developed worldwide. The complex business interactions among the multiple participants introduce new security problems, and the validation flaw is one of the main issues. A legal user can utilize the validation flaws, by some special behaviours, to obtain illegal interests. To deal with above issue, we propose the process to analyze validation flaws by formal methods based on CPN (Coloured Petri nets). The modeling method is based on CPN Modeling Language, and the analyzing process utilizes the transaction properties of online shopping systems. CPN tools can provide the basic support to the analyzing process. A case study throughout this work is used to illustrate the proposed methodology.

A smart contract is a computer protocol intended to digitally facilitate and enforce the negotiation of a contract in undependable environment. However, the number of attacks using the vulnerabilities of the smart contracts is also growing in recent years. Many solutions have been proposed in order to deal with them, such as documenting vulnerabilities or setting the security strategies. Among them, the most influential progress is made by the formal verification method. In this paper, we propose a formal verification method based on Colored Petri Nets (CPN) to verify smart contracts in blockchain system. First, we develop the smart contract models with possible attacker models based on hierarchical CPN modeling, then the smart contract models are executed by step-by-step simulation to validate their functional correctness, and finally we utilize the branch timing logic ASK-CTL based model checking technology in the CPN tools to detect latent vulnerabilities in smart contracts. We demonstrate that our CPN modeling based verification method can not only detect the logical vulnerabilities of the smart contract, but also consider the impacts of users behavior to find out potential non-logical vulnerabilities in the contracts, such as the vulnerabilities caused by the limitations of the Solidity language.

International audience; Featured Application: This paper allowed us to implement Petri net controllers on PLCs (Programmable Logic Controller) of the Flexible Manufacturing System (FMS) in the university of UFR MIM in Metz-FRANCE. Our teamwork applied this control model to the FMS recently installed in our laboratory LGIPM using all the appropriate software (Siemens STEP7 and SCHNEIDER Unity Pro for control software, simulation, and modeling software: CPN Tools and finally supervision software: WINCC FLEXIBLE). Abstract: This study attempted to calculate an optimal Petri net supervisor able to respect the control specifications imposed for a flexible manufacturing system. There are several theories around the control synthesis of discrete event systems. Unfortunately, these methods are very sensitive to the combinatorial explosion of states in the generated graph, especially when the complexity of the system increases. It is therefore necessary to move towards new ways based on formal methods allowing the synthesis of a supervisor. In this work, we propose an algebraic approach using the theory of regions. Our main contribution is to design a set of Petri net controllers based on the properties of Petri nets and not on reachability graph generation for bounded Petri nets. This will decrease significantly the production cost of the manufacturing system, since the computation burden of the supervisor is reduced. Our control policy was applied to a flexible manufacturing system implemented in our laboratory. Comparisons with previous studies using CPLEX software are provided in order to illustrate the effectiveness of our proposed method.

This paper presents a method for the monitoring of deadlock-freeness scenarios in Web Services composition. This method considers the Petri net theory and is based on the analysis of Linear Logic proof trees with dates. In the proposed method, a Linear Logic proof tree with date is built for each different deadlock-freeness scenario in the composed system. These proof trees are analysed and the data obtained from them are used to guide the execution of such scenarios, avoiding the deadlock situations. The CPN Tools is used for the implementation and analysis of a monitored model to evaluate the efficacy of the proposed method.

With the increasing complexity of dynamic concurrent systems, a phase of formal specification and formal verification is needed. UML state machines are widely used to specify dynamic systems behaviours. However, the official semantics of UML is described in a semi-formal manner, which renders the formal verification of complex systems delicate. In this paper, we propose a formalisation of UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, variables), the hierarchy induced by composite states and their associated activities, external, local or inter-level transitions, entry/exit/do behaviours, transition priorities, and shallow history pseudostates. We use a CD player as a motivating example, and run various verifications using CPN Tools.

Aspect-oriented modeling can uncover potential design faults, yet most existing work fails to achieve both separation and composition in a natural and succinct way. This study presents an aspect-oriented modeling and analysis approach with hierarchical Coloured Petri Nets (HCPN). HCPN has sub-models and well-defined semantics combining a set of submodels. These two characteristics of HCPN are nicely integrated into aspect oriented modeling. Submodels are used to model aspects while the combination mechanism contributes to aspects weaving. Furthermore, the woven aspect oriented HCPN model can be simulated and analyzed by the CPN Tools. A systematic web application case study is conducted. The results show the system original properties are satisfied after weaving aspects and all design flaws are revealed. As such, the approach can support web application design and analysis in an aspect-oriented fashion concisely and effectively.

The most common type of short circuit in a three-phase system is a single-phase-to-ground short circuit, accounting for 70 to 90% of electrical faults. In this paper simulation of the protective device from single-phase-to-ground short circuit with automatic change of current setting in electrical networks of 6-10 kV voltage on the basis of Coloured Petri Net is considered. The complexity of elaborated technical systems makes the problem of their modelling actual at the stage of development with the purpose of obtaining estimations of prospective and achievable characteristics. Now the modelling theory of the dynamic discrete systems, based on the formalism of Coloured Petri Nets has a wide application. Petri Net, describing the device operation, was designed and analysed using CPN Tools Programm. The resulting Petri net is correct, as it is live, reversible and safe. Thereby designed device can provide the selective protection from single-phase-to-ground short circuit.

Coloured Petri nets are a formal method that allows to create sophisticated event-driven models. In addition, there exists a software tool, called CPN Tools, which provides a support for creation, simulation and state space-based verification of CPN models. An interesting feature of CPN Tools is that it uses CPN ML, a slightly modified version of the SML functional language, for data manipulation. In this chapter we describe basic concepts of Coloured Petri nets (CPN), SML and CPN ML and by means of an example illustrate how CPN ML can be used to build a concrete, timed CPN model from an abstract, low-level Petri net model in such a way that the structure of the abstract model is preserved. We also explore possibilities of already existing SML code utilization in CPN models.

UML sequence diagrams are used to graphically describe the message interactions between the objects participating in a certain scenario. Combined fragments extend the basic functionality of UML sequence diagrams with control structures, such as sequences, alternatives, iterations, or parallels. In this paper, we present a UML profile to annotate sequence diagrams with combined fragments to model timed Web services with distributed resources under the publish/subscribe paradigm. This profile is exploited to automatically obtain a representation of the system based on Colored Petri nets using a novel model-to-model (M2M) transformation. This M2M transformation has been specified using QVT and has been integrated in a new add-on extending a state-of-the-art UML modeling tool. Generated Petri nets can be immediately used in well-known Petri net software, such as CPN Tools, to analyze the system behavior. Hence, our model-to-model transformation tool allows for simulating the system and finding design errors in early stages of system development, which enables us to fix them at these early phases and thus potentially saving development costs.

In order to satisfy the requirements of International Civil Aviation Organization (ICAO) for aircraft taxi route planning in Advanced Surface Movement Guidance and Control System (A-SMGCS), an airport surface operation modelling and simulation approach based on timed and coloured Petri net is presented. According to the layout of the airport surface and the features of surface operation units, a static Petri net model of the airport surface is established. On this basis, in line with the requirements on the aircraft taxiing velocity in ICAO DOC 9830, the dynamic Petri net model of the airport surface operation is established by adding the time attribute to the static model. Additionally, the method of defining the capacity of airport operation unit place is proposed and the constraints of the airport surface operation are incorporated using Petri net elements. Unlike other papers in the field, the airport surface Petri net model established in this paper can simulate conflict-free taxiing using a Petri net simulator without relying on other model-independent algorithms. Based on the CPN Tools software, taking Toulouse Airport as an example, the validity of the model has been verified by comparing the model running data with real flight data.

Due to the uncertainty of concurrency, the detection of algorithm error of multithreading concurrent software is very difficult, and it is difficult to guarantee the correctness. This paper proposes an automatic model generation method, which automatically reads the multithreading JAVA program and generates the Hierarchical Coloured Petri Nets (HCPN) model consistent with the program behavior. Firstly, reading and analyzing the program source program, storing function declarations in the function list, storing global variables in the global variable list, and building a local variable list and a statement binary tree for each function. Secondly, the multithreading program is converted to a HCPN model. Variables in the program correspond to the token-flowing supported by the variable group in the model. The function calls correspond to substitution transitions in the model. Global variables exist in the whole model, and the local variables exist in the function, the subpage model correspond to the function. The preorder traversal statement binary tree obtains the nested or sequential relationships between the statements, converting the program statement into model fragments and then connecting into a complete HCPN model according to the relationship between the statements. Finally, generating a model file conforming to the CPN Tools file format. So that ASK-CTL model checking method in CPN Tools could be used on the generated model for demand attributes, which detecting algorithm errors. Models generated by this method are consistent with source programs, so model errors in model checking are also program errors. Experimental results verify the validity and correctness of the proposed method.

The exponential use of time dependant and concurrent embedded systems in safety critical situations demands correctness of their behavior. Early design phase verification techniques allow us to ensure system's safety with minimum cost. In Model Driven Software Engineering (MDSE), Unified Modeling Language (UML) is considered as a standard way to visualize system's design but it is a semiformal language and lacks support for precise verification mechanisms to guarantee system's safety. To solve this issue, we have proposed a model driven approach to formalize timed and concurrent embedded systems using Timed Colored Petri Nets. This paper describes the rules for transformation of timed UML State Machines (source model) to Timed Colored Petri Nets (target model). We have focused on timing and behavioral aspects of concurrent embedded systems. We have also demonstrated the applicability of our approach with the help of a benchmark case study using CPN Tools.