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

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

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

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