In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so o...In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so on. However, there are not too many methods for detecting data-flow errors. This paper defines Petri nets with data operations(PN-DO) that can model the operations on data such as read, write and delete. Based on PN-DO, we define some data-flow errors in this paper. We construct a reachability graph with data operations for each PN-DO, and then propose a method to reduce the reachability graph. Based on the reduced reachability graph, data-flow errors can be detected rapidly. A case study is given to illustrate the effectiveness of our methods.展开更多
Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them...Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them to characterize power and energy systems. This work proposes to adopt an HPN to model and analyze a microgrid that consists of green energy sources. A reachability graph for such a model is generated and used to analyze the system properties.展开更多
Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts wi...Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.展开更多
基金supported in part by the National Key R&D Program of China(2017YFB1001804)Shanghai Science and Technology Innovation Action Plan Project(16511100900)
文摘In order to guarantee the correctness of business processes, not only control-flow errors but also data-flow errors should be considered. The control-flow errors mainly focus on deadlock, livelock, soundness, and so on. However, there are not too many methods for detecting data-flow errors. This paper defines Petri nets with data operations(PN-DO) that can model the operations on data such as read, write and delete. Based on PN-DO, we define some data-flow errors in this paper. We construct a reachability graph with data operations for each PN-DO, and then propose a method to reduce the reachability graph. Based on the reduced reachability graph, data-flow errors can be detected rapidly. A case study is given to illustrate the effectiveness of our methods.
基金supported by the Deanship of Scientific Research(DSR)King Abdulaziz University,Jeddah(23-135-35-HiCi)
文摘Hybrid Petri nets(HPNs) are widely used to describe and analyze various industrial hybrid systems that have both discrete-event and continuous discrete-time behaviors. Recently,many researchers attempt to utilize them to characterize power and energy systems. This work proposes to adopt an HPN to model and analyze a microgrid that consists of green energy sources. A reachability graph for such a model is generated and used to analyze the system properties.
基金Supported by the National Natural Science Foundation of China(No.90818023)the National Basic Research Program of China(No.2010CB328101)+2 种基金Shanghai Science&Technology Research Plan(No.09JC1414200,09510701300)"Dawn"Program of Shanghai Education Commission,Program for Changjiang Scholars and Innovative Research Team in University(PCSIRT),National Major Projects of Scienceand Technology(No.2009ZX01036-001-002:part 5)Natural Science Foundation of Educational Government of Anhui Province(No.KJ2011A086)
文摘Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.
