Verification Of Opacity Problem Based On Hybrid Petri Nets

In the Internet,mobile communication systems,military defense systems,and industrial manufacturing systems,the transmission of information and information flows are ubiquitous.It is important to ensure that the exposure of information transmission does not threaten the security of these systems.The opacity problem based on information transmission is an important information security property of a system.Currently,the research on opacity problem is mainly based on discrete event systems.A hybrid Petri net is a graphical modeling tool for hybrid systems that includes both discrete information transmission and continuous information flow.The research of the opacity problem based on hybrid Petri nets has practical significance.The main work of this thesis is on the opacity of hybrid Petri nets.In this thesis,based on states of transitions and markings,four novel definitions of opacity in hybrid Petri nets are proposed,and the corresponding verifying methods are provided.After the transition states of hybrid Petri nets are abstracted,the definition of the work state is proposed,and the system evolution graph is calculated based on the work state.Based on the work state,when the intruder's observation is limited to a given observable event e,we give the definition of the current work state e-opacity of the hybrid Petri net.The e-observer and e-observer construction methods are proposed,and the e-observer is used to verify the current work state e-opacity of the hybrid Petri net.When the intruder can start to observe at any time while the hybrid Petri net is running,we present the definition of the current work state opacity of the hybrid Petri net.The method of verifying the current work state opacity is to verify all current work state e-opacities of the hybrid Petri net,and comprehensively verify the results to determine whether the current work state opacity is satisfied.The difference between the two types of opacity is whether to restrict the intruder's observation of the system.Similarly,based on work states,this work also proposes the definition and verification method of the initial work state opacity of hybrid Petri nets.The work state describes the evolution of the system through the state of transitions in the hybrid Petri net.According to the state of places in the hybrid Petri net,a marking can also describe the evolution of the system.According to the characteristic of the piecewise linear evolution of a hybrid Petri net,this thesis gives the definition of the time-period reachable set to represent all the reachable markings of the hybrid Petri net in a time period.The reachability graph of the hybrid Petri net is composed of all time-period reachability sets.After using generalized mutual exclusion constraints(GMECs)to restrict the value range of secret markings,according to the time occupied by the secret markings in the time-period reachable set,we propose the definition of the secret exposure rate,and quantitative definition of the current state opacity of the hybrid Petri net,respectively.After the e-observer is extended,the current state opacity of the hybrid Petri net can be quantitatively analyzed such that the hybrid Petri net partially satisfies,fully satisfies,and completely does not satisfies the current state opacity.