片上系統(tǒng)總線協(xié)議的形式化建模與模型檢驗分析.pdf

1、基于IP復(fù)用的片上系統(tǒng)設(shè)計方法的出現(xiàn),推動了片上總線技術(shù)的誕生。片上總線協(xié)議是片上總線技術(shù)的核心,其設(shè)計的好壞對片上系統(tǒng)的可靠性有著重大影響。對片上總線協(xié)議的可靠性驗證分析逐漸引起人們的關(guān)注。
　　與傳統(tǒng)的通信協(xié)議、網(wǎng)絡(luò)安全協(xié)議相比,片上總線協(xié)議具有以下特點:交互過程復(fù)雜、傳輸速率高、流水線高級傳輸特性等。正是由于片上總線協(xié)議的這些特點和復(fù)雜性,使得片上系統(tǒng)容易出現(xiàn)潛在的安全問題,同時也為片上總線協(xié)議的有效建模及驗證提出了挑戰(zhàn)。形

2、式化驗證是分析安全協(xié)議的一種有效途徑。針對片上總線協(xié)議的上述特點及挑戰(zhàn),本文對片上總線協(xié)議的形式化建模和模型檢驗分析進行了研究,主要取得以下研究成果:
　　(1)針對Wishbone總線自身特點和復(fù)雜性,提出了一種適用于Wishbone總線協(xié)議的形式化建模方法。首先建立了共享總線互聯(lián)的IP交互模型,基于此模型給出了協(xié)議的有限狀態(tài)機建模方法;然后用CTL對總線協(xié)議的無饑餓屬性、公平性和互斥性進行了形式化規(guī)約。
　　(2)針對A

3、valon總線的特殊技術(shù)架構(gòu)給出了一種有限狀態(tài)機分析模型。首先建立了交換式總線架構(gòu)下的多任務(wù)系統(tǒng)模型,并在該模型的基礎(chǔ)上,深入研究了協(xié)議的交互過程,對該過程采用有限狀態(tài)機進行了嚴(yán)格的刻畫;再用CTL對總線協(xié)議的活性、互斥性和流水線清除屬性進行了形式化描述。
　　(3)基于模型檢驗技術(shù),采用SMV對(1)和(2)中的形式化模型進行了分析驗證,發(fā)現(xiàn)了Wishbone總線存在安全缺陷。該研究表明了本文提出的形式化建模方法的有效性,同時也