Trustworthy Network Control Model And Its Formal Analysis

Fast development in new services and applications of Internet leads to large scale, service diversity and heterogeneity, the controllability and trustworthiness of current network is challenged seriously. How to build a trustowrthy and controllable network is becoming one of essential goals. It is an important means to confirm the trustworthness of network control. However, we are now at the start point of this research field, a rrustworthy network control model is urgent need to achive it. Furermore, to get uniform description about functions, performance and trustworhness of the model, formal describing way should be given. In addition, kinds of formal analysis methods about controllability and trustworthness should be established. For the purpose of solving the above-mentioned questions, based on the Trustworthy and Controllable Network, the dissertation thoroughly studies the trustworthy network control model and its formal analysis methods.Firstly, from the perspective of increasing the credibility of data collecting and shareing, improving the trustworthness of analyzing and decision-making, strengthening the reliability of control command executing, a trustworthy network control model named as TCM is proposed which is to surport cross-layer monitoring, synergistically reasoning, concentrlized policy decision and trusted implementing. Next, Q-algbra is introduced to depict trusted feature and Generation Stochastic High Level Petri Net with Q-algbra is defined, Q-GSHLPN for short. Transition firing and trusted feature assembling rules are confirmed and a formal description of TCM using Q-GSHLPN is given. Thirdly, to analyse the controllability of TCM, two algorithms are designed. One is called determing of Leagle Firing Transiton sequence which can be used to verify control fuction of TCM. Another is reachablity judgement based on process of Petri Net which is used to forecast the functional ability of TCM. Finally, aimed at the diffirence of qualitatively and quantitatively analyzing of TCM, a kind of ctedibility decribing logic and satisfying relations are established to judge the trusted property of TCM. Simulating relation and credible distance are defined and a calculating way of global trustworthy degree based on multi-dimension credible feature is given to gain quantitative trustworthness.In conclusion, the trustworthy network control model and its formal analysis are thoroughly explored in this dissertation.Results from theoretical demonstration and instance analysis shows the correctness and effectiveness of TCM and the availability to guide the construction of trustworthy control mechnism.