The paper presents an improved cellular automaton model according to the feature of evacuation near the outlet. We studied friction and turning factors that affect pedestrian evacuation speed. By using mathematical me...The paper presents an improved cellular automaton model according to the feature of evacuation near the outlet. We studied friction and turning factors that affect pedestrian evacuation speed. By using mathematical methods to derive expressions of friction function and turning function. The average pedestrian outflow of the simulation that includes the effect of both the frictional function and the turning function agrees well with experiment result. On the contrary, the simulation results that only include the effect of the frictional function are not corresponding to the experiment results well. Simulation results show that friction and turning can not be ignored. By analyzing the simulation results, it verified that the model can accurately reflect the actual evacuation process and has practical value.展开更多
Moving target defense （MT_D） is a novel way to alter the asymmetric situation of attacks and defenses, and a lot of MTD studies have been carried out recently. However, relevant analysis for the defense mechanism of...Moving target defense （MT_D） is a novel way to alter the asymmetric situation of attacks and defenses, and a lot of MTD studies have been carried out recently. However, relevant analysis for the defense mechanism of the MTD technology is still absent. In this paper, we analyze the defense mechanism of MTD technology in two dimensions. First, we present a new defense model named MP2R to describe the proactivity and effect of MTD technology intuitively. Second, we use the incomplete information dynamic game theory to verify the proactivity and effect of MTD technology. Specifically, we model the interaction between a defender who equips a server with different types of MTD techniques and a visitor who can be a user or an attacker, and analyze the equilibria and their conditions for these models. Then, we take an existing incomplete information dynamic game model for traditional defense and its equilibrium result as baseline for comparison, to validate the proactivity and effect of MTD technology. We also identify the factors that will influence the proactivity and effectiveness of the MTD approaches. This work gives theoretical support for understanding the defense process and defense mechanism of MTD technology and provides suggestions to improve the effectiveness of MTD approaches.展开更多
In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the sa...In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.展开更多
文摘The paper presents an improved cellular automaton model according to the feature of evacuation near the outlet. We studied friction and turning factors that affect pedestrian evacuation speed. By using mathematical methods to derive expressions of friction function and turning function. The average pedestrian outflow of the simulation that includes the effect of both the frictional function and the turning function agrees well with experiment result. On the contrary, the simulation results that only include the effect of the frictional function are not corresponding to the experiment results well. Simulation results show that friction and turning can not be ignored. By analyzing the simulation results, it verified that the model can accurately reflect the actual evacuation process and has practical value.
基金Project supported by the National Basic Research Program(973)of China(No.2012CB315906)
文摘Moving target defense （MT_D） is a novel way to alter the asymmetric situation of attacks and defenses, and a lot of MTD studies have been carried out recently. However, relevant analysis for the defense mechanism of the MTD technology is still absent. In this paper, we analyze the defense mechanism of MTD technology in two dimensions. First, we present a new defense model named MP2R to describe the proactivity and effect of MTD technology intuitively. Second, we use the incomplete information dynamic game theory to verify the proactivity and effect of MTD technology. Specifically, we model the interaction between a defender who equips a server with different types of MTD techniques and a visitor who can be a user or an attacker, and analyze the equilibria and their conditions for these models. Then, we take an existing incomplete information dynamic game model for traditional defense and its equilibrium result as baseline for comparison, to validate the proactivity and effect of MTD technology. We also identify the factors that will influence the proactivity and effectiveness of the MTD approaches. This work gives theoretical support for understanding the defense process and defense mechanism of MTD technology and provides suggestions to improve the effectiveness of MTD approaches.
基金supported by the New Century Excellent Researcher Award Program from Ministry of Education of China (Grant No. NCET-07-0059)the Fundamental Research Funds for the Central Universities (Grant No.2011YJS006)+1 种基金the National High Technology Research and DevelopmentProgram of China ("863" Program) (Grant No. 2011AA010104)the State Key Laboratory of Rail Traffic Control and Safety Research Project(Grant Nos. RCS2008ZZ001, RCS2008ZZ005)
文摘In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.
