Narrow Results

Semilinearity plays a key role not only in formal languages but also in the study of Petri nets. Although the reachability set of a Petri net may not be semilinear in general, there are a wide variety of subclasses of Petri nets which enjoy having semilinear reachability sets. In this paper, we develop sufficient conditions for Petri nets under which semilinearity is guaranteed. Our approach, based on the idea of path decomposition, can be used for consolidating several existing semilinearity results as well as for deriving new results all under the same framework.

Reaction networks, or equivalently Petri nets, are a general framework for describing processes in which entities of various kinds interact and turn into other entities. In chemistry, where the reactions are assigned ‘rate constants’, any reaction network gives rise to a nonlinear dynamical system called its ‘rate equation’. Here we generalize these ideas to ‘open’ reaction networks, which allow entities to flow in and out at certain designated inputs and outputs. We treat open reaction networks as morphisms in a category. Composing two such morphisms connects the outputs of the first to the inputs of the second. We construct a functor sending any open reaction network to its corresponding ‘open dynamical system’. This provides a compositional framework for studying the dynamics of reaction networks. We then turn to statics: that is, steady state solutions of open dynamical systems. We construct a ‘black-boxing’ functor that sends any open dynamical system to the relation that it imposes between input and output variables in steady states. This extends our earlier work on black-boxing for Markov processes.

An original knowledge representation scheme named KRP based on Petri net theory is proposed. The formal description of the scheme, and the inference procedure similar to "intersection search" in semantic networks, are given.

Reconfigurable systems have been recently used in many domains. Although the concept of multi-context logic controllers is relatively new, it may be noticed that the subject is receiving a lot of attention, especially in the industry. The work constitutes a stepping stone in design of reconfigurable logic controllers towards bridging the gap between Petri nets, their decomposition, formal verification and implementation with the use of FPGA structures with the possibility of further partial reconfiguration. The paper proposes a new design concept of reconfigurable logic controllers, implemented with the FPGA device. A logic controller is formally described by a Petri net and decomposed into separate sequential modules. Optional versions (contexts) of the selected module may be prepared additionally. Depending on the needs, a particular module can be replaced by either version (context) with the use of the partial reconfiguration technique. To avoid formal errors and mistakes, the proposed design path is supported by formal verification with the model checking methods based on the rule-based logical model. The proposed design concept has been verified experimentally with the application of Xilinx FPGA devices.

This paper presents the formal verification method for high-level synthesis (HLS) to detect design errors of dataflow algorithms by using Petri Net (PN) and symbolic-model-verifier (SMV) techniques. Formal verification in high-level design means architecture verification, which is different from functional verification in register transfer level (RTL). Generally, dataflow algorithms need algorithmic transformations to achieve optimal goals and also need design scheduling to allocate processor resources before mapping on a silicon. However, algorithmic transformations and design scheduling are error-prone. In order to detect high-level faults, high-level verification is applied to verify the synthesis results in HLS. Instead of applying Boolean algebra in traditional verification, this paper adopts both Petri Net theory and SMV model checker to verify the correctness of the synthesis results of the high-level dataflow designs. In the proposed hybrid verification method, a high-level design or DUV (design-under-verification) is first transformed into a Petri Net model. Then, Petri Net theory is applied to check the correctness of its algorithmic transformations of HLS, and the SMV model checker is used to verify the correctness of the design scheduling. We presented two approaches to realize the proposed verification method and concluded the best one who outperforms the other in terms of processing speed and resource usage.

High-performance radio-frequency identification (RFID) is a challenging issue for large-scale enterprises. As a key component of an RFID system, RFID middleware is an important factor to measure the performance of the system. To evaluate the feasibility of an RFID middleware, the performance of the RFID middleware should be carefully evaluated in various RFID-enabled business environments. However, the construction of an RFID testbed requires a lot of time, money, and human resources because it involves numerous tagged items and a large number of deployed readers. We must provide a meaningful input tag stream representing various business activities, rather than random data. This paper presents a novel simulation model for the virtual construction of RFID testbeds. To ensure the semantic validity of the input tag stream, the proposed RFID simulation network (RSN) extends Petri nets by including sets of functions that represent unique characteristics of RFID environments such as the uncertainty of communications and tag movement patterns. By configuring appropriate functions, the RSN automatically generates an input tag stream that matches the distribution of real data. We demonstrate that the RSN model correctly reflects data from real-world environments by comparing input tag streams from real RFID equipment and from the RSN model.

Dealing with crosscutting concerns has been a critical problem in software development processes. To facilitate handling crosscutting concerns at design phases, we proposed an aspect-oriented modeling and integration approach with UML activity diagrams. The primary concerns are depicted with UML activity diagrams as primary models, whereas crosscutting concerns are described with aspectual extended activity diagrams as aspect models. Aspect models can be integrated into primary models automatically. The AOM approach can reduce the complexity of design models. However, potential faults that violate desired properties of the software system might still be introduced during the modeling or integration processes. The verification technique is well-known for its ability to assure the correctness of models and uncover design problems before implementation. We propose a framework to verify aspect-oriented UML activity diagrams based on Petri net verification techniques. For verification purpose, we transform the integrated activity diagrams into Petri nets and prove the consistency of the transformation. Then, crosscutting concerns in system requirements are refined to properties in the form of CTL formulas. Finally, the Petri nets are verified against the formalized properties to report whether the aspect-oriented design models satisfies the requirements. Furthermore, we implement a tool named Jasmine-AOV to support the verification process. Case studies are conducted to evaluate the effectiveness of the proposed approach.

In open and changeful Internet, the enterprise business process needs to be organized or restructured dynamically in order to adapt to environment changes and business logic updates. The solution of Web service and service-oriented architecture (SOA) provides a promising approach. The business processes working as a temporary workflow can be composed by distributed services. However, the cross-organizational service feature of business process requires considering not only the functional requirements but also the timed constraints. The timed property plays an important role in service interactions between business processes, such as timed activity, timeout and timed deadlock. Thus, if time requirements cannot be guaranteed, the new created business process will not be acceptable. In this paper, it proposes a framework of using Petri Net to model timed service business process. First, it defines the behavior model of service business process and gives process composition patterns for different structural forms. Second, service model is extended with time specifications, describing timed constraints among business activity interactions. Third, to support further verifications, it introduces a method for the automatic timed properties generation in the form of temporal logic formulae. Our framework gives a reference in practice to formalize service business process into timed service model.

The feeding unit is an important functional part in the paper industry that requires the development of effective maintenance plan based on its reliability analysis. This study analyzes reliability of the considered unit employing trapezoidal fuzzy numbers in fuzzy $\lambda$–$\tau$ methodology with Petri net modeling. In this analysis, the collected crisp input data of each subsystem has been fuzzified using trapezoidal fuzzy numbers. Then fuzzy values of several reliability factors of feeding unit, namely, failure rate, repair time, reliability, availability, etc. at ±15%, ±25% and ±40% spread levels have been calculated. Further, the obtained fuzzy values of reliability factors have been defuzzified to analyze system behavior of feeding unit. The analysis is useful for plant maintenance and operation management to understand the behavior of feeding unit in a more realistic manner.

Background: Nowadays, service-oriented architectures and cloud-based infrastructures are widely used in manufacturing industries and IT organizations. These architectures and infrastructures are based on shared system resources. In some organizations, system resources like a printer, photocopy machines, and scanners are also shared among the members of the organization. The purpose of the proposed work is to model various types of shared system resources, shared system resources based architecture/infrastructure and analyze the model to identify the possible security risk associated with shared system resources and shared system resources based architecture/infrastructure.

Design Approach: To model shared system resources and shared system resources based architecture/Infrastructure, Petri net and its variations are used. For security analysis of the Petri net based model of the shared system resource, Petri net algebra based concepts are applied.

Results: The present paper successfully demonstrates that the proposed Petri net based modeling approach can be used for quantitative and qualitative security analysis of shared system resources and shared system resources based architecture/infrastructure. For quantitative analysis of security risk associated with shared system resources, information theoretic concepts are used. To demonstrate the effectiveness of the proposed method, case studies are also incorporated in the present paper. The proposed approach can take various security risk factors like timing analysis attack, information leakage due to confidentiality policy violation and power analysis attack into the consideration while analyzing the security of shared system resources in the industrial environment.

This paper introduces an interactive Memex-like application using a self-modifiable Petri Net model — Self-modifiable Color Petri Net (SCPN). The Memex ("memory extender") device proposed by Vannevar Bush in 1945 focused on the problems of "locating relevant information in the published records and recording how that information is intellectually connected". The important features of Memex include associative indexing and retrieval. In this paper, the self-modifiable functions of SCPN are used to achieve trail recording and retrieval. A place in SCPN represents a website and an arc indicates the trail direction. Each time when a new website is visited, a place corresponding to this website will be added. After a trail is built, users can use it to retrieve the websites they have visited. Besides, useful user interactions are supported by SCPN to achieve Memex functions. The types of user interactions include the following — forward, backward, history, search, etc. A simulator has been built to demonstrate that the SCPN model can realize Memex functions. Petri net instances can be designed to model trail record, back, and forward operations using this simulator. Furthermore, a client-server based application system has been built. Using this system, a user can surf online and record his surfing history on the server according to different topics and share them with other users.

Petri nets are a discrete event simulation approach developed for system representation, in particular for their concurrency and synchronization properties. Various extensions to the original theory of Petri nets have been used for modeling molecular biology systems and metabolic networks. These extensions are stochastic, colored, hybrid and functional. This paper carries out an initial review of the various modeling approaches based on Petri net found in the literature, and of the biological systems that have been successfully modeled with these approaches. Moreover, the modeling goals and possibilities of qualitative analysis and system simulation of each approach are discussed.

The purpose of this paper is to discuss how to model and analyze signaling pathways by using Petri net. Firstly, we propose a modeling method based on Petri net by paying attention to the molecular interactions and mechanisms. Then, we introduce a new notion "activation transduction component" in order to describe an enzymic activation process of reactions in signaling pathways and shows its correspondence to a so-called elementary T-invariant in the Petri net models. Further, we design an algorithm to effectively find basic enzymic activation processes by obtaining a series of elementary T-invariants in the Petri net models. Finally, we demonstrate how our method is practically used in modeling and analyzing signaling pathway mediated by thrombopoietin as an example.

Embedded multimedia systems often run multiple time-constrained applications simultaneously. To meet the throughput constraints given in the specification, each application must be provided with enough resources by the underlying architecture, which is generally a multiprocessor system-on-chip (MPSoC). For this purpose, a mechanism for task binding and scheduling is required to provide each application with a timing guarantee, keeping in mind the available resources like processor(s) and memory bandwidth. Commonly, synchronous dataflow graphs (SDFGs) are used to model time-constrained multimedia applications. There are resource allocation strategies for SDFGs that help in formulating efficient techniques for calculating the throughput of a bounded and scheduled SDFG. The strategies are effective in terms of run-time and allocated resources. However, there is no unified modeling technique to simultaneously represent the application and the underlying architecture with resource allocation. This paper discusses a novel modeling technique using Colored Timed Petri Nets (CTPNs), which can be used to model the application as well as the architecture and the resource allocation. Such a representation helps in checking properties like liveness and boundedness for the application, taking into account the resource allocation and thus helping in defining satisfactory schedules for the executable tasks.

Web service is the basic unit of service-oriented architecture (SOA), and it is a new type of Web application. Web service composition is a technology that forms a new service by combining multiple services, and the function of new service is more diverse. However, due to the complexity of the functions and the concurrency of the composite process, the new service may not be correct. Therefore, it is very important to verify the interactive behavior of Web service composition. A method for verifying the interaction of Web service composition by combining Petri net with symbol model checking is proposed. The conversion rules between Petri net model and NuSMV language are proposed. Among them, Petri net model is modeled based on BPEL process. Finally, the automatic verification and temporal logic verification of Petri net model of Web service composition are realized. Also, the feasibility and correctness of the method are illustrated by verifying the ShippingService.

Petri nets are a powerful tool for visual representation of complex software engineering and knowledge engineering problems, and for analysis of their dynamic behavior. This survey consists mainly of practical examples, which include the use of time Petri nets. Petri nets have well-defined semantics, and can be used to interpret textual languages, particularly for communication and coordination. We explore one such application in detail. The nets can grow too large for human comprehension; some suggestions are given on how to deal with this problem. We also look at fuzzy reasoning based on Petri nets.

The Petri net method is a reliable and accurate way of analyzing protocol, albeit with limitations in resolving conflicts between protocol performance evaluation and the protocol validation. A methodology of using original Petri net as a model of protocol verification is proposed to solve this problem. Without changing any part of the structure of the original Petri net, the method introduces protocol performance evaluation by attaching time delay to transition, hence avoiding repeat modeling. Therefore, the model can evaluate the performance of the protocol and validate it at the same time. As an example, the paper validates 0-1 stop and wait for protocol in detail and then evaluates the performance of the protocol by translating original Petri net of 0-1 stop and wait for protocol into timed Petri net.

In this paper we present in a tutorial fashion the framework of reaction systems — a formal approach to investigating processes instigated by the living cell. The main idea behind this approach is that this functioning is determined by interactions between biochemical reactions, and these interactions are based on two mechanisms, facilitation and inhibition.

Petri net is an important tool for discrete event dynamic systems modeling and analysis. And it has great ability to handle concurrent phenomena and non-deterministic phenomena. Currently Petri nets used in wind turbine fault diagnosis have not participated in the actual system. This article will combine the existing fuzzy Petri net algorithms; build wind turbine control system simulation based on Siemens S7-1200 PLC, while making matlab gui interface for migration of the system to different platforms.