家庭信息化程度正随着3C行业的快速发展而逐步地提高,网络化、智能化的趋势已经成为数字家庭产业的共识。数字家庭网络化的目的在于通过建构完整的家庭网络架构,进行内部设备的互联互通,同时将外部公共网络和应用延伸至家庭,从而实现数据通信、娱乐和共享等各种功能。数字家庭无线射频协议正是在这样的需求下被制定出来。数字家庭无线射频协议提高了家庭内部设备之间通信的易用性和可靠性,为设备的互动建立了技术基础,从而实现了家庭内部网络的信息共享和互联互通,使得控制器在射频中继器的协助下,实现对终端设备的监控。鉴于其在数字家庭技术体系中的重要性,本文使用基于Petri网的形式化方法对协议本身和相关系统进行建模和分析,为进一步研究和应用该协议提供了一种新的思路。所做的工作主要有如下几个方面。(1)对数字家庭无线射频通讯协议和Petri网基本理论进行了详细的介绍,接着将协议按参与者角色分成了三个部分,分别使用Petri网对其进行建模与分析,最终验证了协议的正确性和完整性。(2)针对终端设备的注册原语和会话层、网络层、链路层的通信机制,假设了若干不安全因素,用Petri网建立了入侵者模型,通过对模型的分析,得到相应的应对方案。(3)提出了一种基于射频协议的自动注册和路径更新系统,弥补了终端设备注册申请的缺陷和射频中继器意外故障的情况。接着使用可达图等Petri网分析技术对系统中的两种新功能进行验证,从而得到系统的若干重要性质。