The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,...The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed QuantumNets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net(CPN)Tools.Moreover,reachability tree(RT)analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.展开更多
The planning and scheduling in real shop floor is actually achieved by coordination between different persons. In this process, cooperation is mainstream, but competition also exists, for example, the competition betw...The planning and scheduling in real shop floor is actually achieved by coordination between different persons. In this process, cooperation is mainstream, but competition also exists, for example, the competition between different groups, operators with the same skill, etc. In multi-agent based shop floor management and control system, this competition and cooperation relation must be embodied. The general process of shop floor production planning and scheduling is studied, and a colored Petri-net model for the competition and cooperation process of three main agents in such system to achieve shop floor production planning and scheduling is presented. The evaluating method of bids in bidding process that especially embodies the competition relationship is also presented. This colored Petri-net model gives a clear illustration of this complex coordination process to system designers, effectively promotes the cooperative development.展开更多
A new ball passing strategy for robot soccer is proposed in this paper. With introduce of a new algorithm on ball passing, the optimum strategy is confirmed to be more efficient and exact when passing a ball. Question...A new ball passing strategy for robot soccer is proposed in this paper. With introduce of a new algorithm on ball passing, the optimum strategy is confirmed to be more efficient and exact when passing a ball. Questions of role switching in multi-intelligent agent cooperation in robot soccer are described based on Generalized Stochastic Petri-Net （GSPN）. Results of computer simulation have confirmed the feasibility and efficiency of above Petri-net method.展开更多
Activity is now playing a vital role in software processes. To ensure the high-level efficiency of software processes, a key point is to locate those activities that own bigger resource occupation probabilities with r...Activity is now playing a vital role in software processes. To ensure the high-level efficiency of software processes, a key point is to locate those activities that own bigger resource occupation probabilities with respect to average execution time, called delayed activities, and then improve them. To this end, we firstly propose an approach to locating delayed activities in software processes. Furthermore, we present a case study, which exhibits the high-level efficiency of the approach, to concretely illustrate this new solution. Some beneficial analysis and reasonable modification are developed in the end.展开更多
文摘The formal modeling and verification of aircraft takeoff is a challenge because it is a complex safety-critical operation.The task of aircraft takeoff is distributed amongst various computer-based controllers,however,with the growing malicious threats a secure communication between aircraft and controllers becomes highly important.This research serves as a starting point for integration of BB84 quantum protocol with petri nets for secure modeling and verification of takeoff procedure.The integrated model combines the BB84 quantum cryptographic protocol with powerful verification tool support offered by petri nets.To model certain important properties of BB84,a new variant of petri nets coined as Quantum Nets are proposed by defining their mathematical foundations and overall system dynamics,furthermore,some important system properties are also abstractly defined.The proposed QuantumNets are then applied for modeling of aircraft takeoff process by defining three quantum nets:namely aircraft,runway controller and gate controller.For authentication between quantum nets,the use of external places and transitions is demonstrated to describe the encryptiondecryption process of qubits stream.Finally,the developed takeoff quantum network is verified through simulation offered by colored petri-net(CPN)Tools.Moreover,reachability tree(RT)analysis is also performed to have greater confidence in feasibility and correctness of the proposed aircraft takeoff model through the Quantum Nets.
基金Supported partly by the Hi-tech Program of China( China86 3) ( No.86 3-5 11-943-0 0 9) and the National Natural Sci-ence Foundation of China( No.5 9990 470 )
文摘The planning and scheduling in real shop floor is actually achieved by coordination between different persons. In this process, cooperation is mainstream, but competition also exists, for example, the competition between different groups, operators with the same skill, etc. In multi-agent based shop floor management and control system, this competition and cooperation relation must be embodied. The general process of shop floor production planning and scheduling is studied, and a colored Petri-net model for the competition and cooperation process of three main agents in such system to achieve shop floor production planning and scheduling is presented. The evaluating method of bids in bidding process that especially embodies the competition relationship is also presented. This colored Petri-net model gives a clear illustration of this complex coordination process to system designers, effectively promotes the cooperative development.
文摘A new ball passing strategy for robot soccer is proposed in this paper. With introduce of a new algorithm on ball passing, the optimum strategy is confirmed to be more efficient and exact when passing a ball. Questions of role switching in multi-intelligent agent cooperation in robot soccer are described based on Generalized Stochastic Petri-Net （GSPN）. Results of computer simulation have confirmed the feasibility and efficiency of above Petri-net method.
基金supported by National Natural Science Foundation of China(No.61462091)High-tech Industrial Development Program of Yunnan Province(No.1956,in 2012)+2 种基金New Academic Researcher Award for Doctoral Candidates of Yunnan Province of China(No.ynu201414)Natural Science Youth Foundation of Yunnan Province of China(No.2014FD006)the Postgraduates Science Foundation of Yunnan University(No.ynuy201424)
文摘Activity is now playing a vital role in software processes. To ensure the high-level efficiency of software processes, a key point is to locate those activities that own bigger resource occupation probabilities with respect to average execution time, called delayed activities, and then improve them. To this end, we firstly propose an approach to locating delayed activities in software processes. Furthermore, we present a case study, which exhibits the high-level efficiency of the approach, to concretely illustrate this new solution. Some beneficial analysis and reasonable modification are developed in the end.
