The Formal Analysis And Research Of Digital Home RF Protocol

The degree of family information is gradually improved with the rapid development of 3C industry, and the networking and intelligent trend has become the consensus in the digital home. The networkization of digital home is to construct a complete home network architecture and proceed interoperability among the internal devices, while external public network and application are extended to the family, in order to achieve data communication, entertainment and sharing functions. Digital home radio frequency protocol has developed in such circumstances.Digital home radio frequency protocol improves the usability and reliability of communication between devices within the family and establishes the technical foundation for the interaction, so information sharing and interoperability is implemented. Then the controller can monitor the status of terminal device with the assistance of RF repeater. In view of its importance in the digital home technology system, Petri nets are used for modeling and analysis of protocol itself and related system, then a new way of thinking is provided for further study and application of the protocol. Work I has done is as follows.(1) Digital home RF protocol and the basic theory of Petri nets are introduced in detail. Then the protocol is divided into three parts by the role of participants and every part is modeled and analyzed by Petri net. Eventually, the correctness and completeness of protocol is validated.(2) For the registration of terminal device and the communication mechanism of session layer, network layer and link layer, some factors of insecurity are assumed and intruder model is set up by Petri net. Then the corresponding solutions are got by analysis of the model.(3) An automatic registration and dynamic path system based on RF protocol is proposed, which makes up for the defect of registration of terminal device and unexpected failures of RF repeater. Then some analysis techniques of Petri net such as reachability graph are used to verify the two new features in the system arid we can obtain a number of important properties of the system.