基于IP复用的片上系统设计方法的出现,推动了片上总线技术的诞生。片上总线协议是片上总线技术的核心,其设计的好坏对片上系统的可靠性有着重大影响。对片上总线协议的可靠性验证分析逐渐引起人们的关注。　　与传统的通信协议、网络安全协议相比,片上总线协议具有以下特点:交互过程复杂、传输速率高、流水线高级传输特性等。正是由于片上总线协议的这些特点和复杂性,使得片上系统容易出现潜在的安全问题,同时也为片上总线协议的有效建模及验证提出了挑战。形式化验证是分析安全协议的一种有效途径。针对片上总线协议的上述特点及挑战,本文对片上总线协议的形式化建模和模型检验分析进行了研究,主要取得以下研究成果:　　(1)针对Wishbone总线自身特点和复杂性,提出了一种适用于Wishbone总线协议的形式化建模方法。首先建立了共享总线互联的IP交互模型,基于此模型给出了协议的有限状态机建模方法;然后用CTL对总线协议的无饥饿属性、公平性和互斥性进行了形式化规约。　　(2)针对Avalon总线的特殊技术架构给出了一种有限状态机分析模型。首先建立了交换式总线架构下的多任务系统模型,并在该模型的基础上,深入研究了协议的交互过程,对该过程采用有限状态机进行了严格的刻画;再用CTL对总线协议的活性、互斥性和流水线清除属性进行了形式化描述。　　(3)基于模型检验技术,采用SMV对(1)和(2)中的形式化模型进行了分析验证,发现了Wishbone总线存在安全缺陷。该研究表明了本文提出的形式化建模方法的有效性,同时也表明了应用模型检验技术对片上总线协议进行分析验证的可行性。