Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurr...Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurrent system, while reachability graph is a serial one. However, concurrency is a kind of property which is not only very significant but also difficult to be analyzed and controlled. This paper presents the concepts of concurrent reachable marking and concurrent reachable graph in order to represent and analyze the concurrent system. The algorithm constructing concurrent reachable marking set and concurrent reachability graph is also shown so that we can study the response problems among services in a network computing environment and analyze the throughput of the system. The Dining Philosophers Problem, which is a classic problem of describing the management of concurrent resources, is given as an example to illustrate the significance of concurrent reachability graph.展开更多
The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic (CTL) allows us to verify the soundness with symbolic model checkers. Therefore the...The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic (CTL) allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic* (CTL*) can be used to character the relaxed soundness of the workflow.展开更多
In this paper, a new analytic method for modeling and evaluating mobile ad hoc networks (MANET) is proposed. Petri nets technique is introduced into MANET and a packet-flow parallel scheduling scheme is presented usin...In this paper, a new analytic method for modeling and evaluating mobile ad hoc networks (MANET) is proposed. Petri nets technique is introduced into MANET and a packet-flow parallel scheduling scheme is presented using Stochastic Petri Nets (SPN). The flowing of tokens is used in graphics mode to characterize dynamical features of sharing a single wireless channel. Through SPN reachability analysis and isomorphic continuous time Markov process equations, some network parameters, such as channel efficiency, one-hop transmission delay etc., can be obtained. Compared with conventional performance evaluation methods, the above parameters are mathematical expressions instead of test results from a simulator.展开更多
According to the requirement of computer forensic and network forensic, a novel forensic computing model is presented, which exploits XML/OEM/RM data model, Data fusion technology, forensic knowledgebase, inference me...According to the requirement of computer forensic and network forensic, a novel forensic computing model is presented, which exploits XML/OEM/RM data model, Data fusion technology, forensic knowledgebase, inference mechanism of expert system and evidence mining engine. This model takes advantage of flexility and openness, so it can be widely used in mining evidence.展开更多
Since the man-machine interfaces (MMI) of a main control room provide the control platform of a nuclear power plant (NPP), the development of the design quality of MMIs plays a very important role in the operation of ...Since the man-machine interfaces (MMI) of a main control room provide the control platform of a nuclear power plant (NPP), the development of the design quality of MMIs plays a very important role in the operation of a NPP. With the development of digital technology, the development of the advanced main control rooms (AMCRs) has become an inexorable trend. Therefore, the positive and the negative effects of AMCRs on human factors engineering need to be evaluated. For this purpose, a simulation system has been studied and developed to quantitatively evaluate a MMI design from the viewpoint of human factors. The simulation system takes advantage of computer simulation technology to simulate an operating process of an interaction between operators and a MMI design under an instruction of an operation procedure of the AMCR of a NPP. Meanwhile, the necessary data are recorded for evaluation. It integrates two editors and one simulator. In the paper, the simulation system is presented in detail. Furthermore, one sample is given to show the results of each of these three subsystems.展开更多
Petri net language is a powerful tool for describing dynamic behaviors of physical systems. However, it is not easy to obtain the language expression for a given Petri net especially a structure-complex net. In this p...Petri net language is a powerful tool for describing dynamic behaviors of physical systems. However, it is not easy to obtain the language expression for a given Petri net especially a structure-complex net. In this paper, we first analyze the behaviors of S-nets, which are structure-simple. With the decomposition method based on a given index function on the place set, a given structure-complex Petri net can be decomposed into a set of structure-simple S-nets. With the language relationships between the original system and the decomposed subnets, an algorithm to obtain the language expression of a given structure-complex net system is presented, which benefits the analysis of physical systems based on the Petri net language.展开更多
文摘Reachability graph is a very important tool to analyze the dynamic properties of Petri nets, but the concurrent relation of transitions in Petri nets cannot be represented by reachability graph. Petri net is a concurrent system, while reachability graph is a serial one. However, concurrency is a kind of property which is not only very significant but also difficult to be analyzed and controlled. This paper presents the concepts of concurrent reachable marking and concurrent reachable graph in order to represent and analyze the concurrent system. The algorithm constructing concurrent reachable marking set and concurrent reachability graph is also shown so that we can study the response problems among services in a network computing environment and analyze the throughput of the system. The Dining Philosophers Problem, which is a classic problem of describing the management of concurrent resources, is given as an example to illustrate the significance of concurrent reachability graph.
基金Supported by the National Natural Science Foun-dation of China (60573046)
文摘The soundness is a very important criterion for the correctness of the workflow. Specifying the soundness with Computation Tree Logic (CTL) allows us to verify the soundness with symbolic model checkers. Therefore the state explosion problem in verifying soundness can be overcome efficiently. When the property is not satisfied by the system, model checking can give a counter-example, which can guide us to correct the workflow. In addition, relaxed soundness is another important criterion for the workflow. We also prove that Computation Tree Logic* (CTL*) can be used to character the relaxed soundness of the workflow.
文摘In this paper, a new analytic method for modeling and evaluating mobile ad hoc networks (MANET) is proposed. Petri nets technique is introduced into MANET and a packet-flow parallel scheduling scheme is presented using Stochastic Petri Nets (SPN). The flowing of tokens is used in graphics mode to characterize dynamical features of sharing a single wireless channel. Through SPN reachability analysis and isomorphic continuous time Markov process equations, some network parameters, such as channel efficiency, one-hop transmission delay etc., can be obtained. Compared with conventional performance evaluation methods, the above parameters are mathematical expressions instead of test results from a simulator.
基金Supported by the Scientific and TechnologicalBureau of the Ministry of Public Security of P.R.China ,the Projectof the Network Supervising Bureau(2005yycxhbst117) the Project ofthe 15th Overall Plan of Education Department of Hubei Province(2004d349) the Project of the 15th Overall Plan of Social ScienceFund of Hubei Province([2005]073)
文摘According to the requirement of computer forensic and network forensic, a novel forensic computing model is presented, which exploits XML/OEM/RM data model, Data fusion technology, forensic knowledgebase, inference mechanism of expert system and evidence mining engine. This model takes advantage of flexility and openness, so it can be widely used in mining evidence.
文摘Since the man-machine interfaces (MMI) of a main control room provide the control platform of a nuclear power plant (NPP), the development of the design quality of MMIs plays a very important role in the operation of a NPP. With the development of digital technology, the development of the advanced main control rooms (AMCRs) has become an inexorable trend. Therefore, the positive and the negative effects of AMCRs on human factors engineering need to be evaluated. For this purpose, a simulation system has been studied and developed to quantitatively evaluate a MMI design from the viewpoint of human factors. The simulation system takes advantage of computer simulation technology to simulate an operating process of an interaction between operators and a MMI design under an instruction of an operation procedure of the AMCR of a NPP. Meanwhile, the necessary data are recorded for evaluation. It integrates two editors and one simulator. In the paper, the simulation system is presented in detail. Furthermore, one sample is given to show the results of each of these three subsystems.
基金This work was supported by the National Natural Science Foundation of China(No.60173053&No.60274063)the Excellent Young Scientist Foundation of Shandong Province of China(No.02BS069).
文摘Petri net language is a powerful tool for describing dynamic behaviors of physical systems. However, it is not easy to obtain the language expression for a given Petri net especially a structure-complex net. In this paper, we first analyze the behaviors of S-nets, which are structure-simple. With the decomposition method based on a given index function on the place set, a given structure-complex Petri net can be decomposed into a set of structure-simple S-nets. With the language relationships between the original system and the decomposed subnets, an algorithm to obtain the language expression of a given structure-complex net system is presented, which benefits the analysis of physical systems based on the Petri net language.
