核電廠FPGA儀控系統(tǒng)的驗(yàn)證研究.pdf

1、FPGA(Field-Programmable Gate Array)在核工業(yè)領(lǐng)域仍然是一項(xiàng)新興技術(shù)，目前國內(nèi)外尚無可用于指導(dǎo)核電廠FPGA儀控系統(tǒng)開發(fā)和許可的統(tǒng)一導(dǎo)則和標(biāo)準(zhǔn)。核電廠FPGA應(yīng)用的挑戰(zhàn)在于難以驗(yàn)證它的安全性和可靠性。因此，亟需一套能夠指導(dǎo)開發(fā)和許可核電廠FPGA系統(tǒng)的導(dǎo)則和標(biāo)準(zhǔn)，研究具有可操作性的開發(fā)與驗(yàn)證技術(shù)，為核電廠FPGA安全級儀控系統(tǒng)的驗(yàn)證與確認(rèn)(V&V)和評審提供理論和技術(shù)參考。
　　首先，本文基于美國核

2、管會(huì)(NRC)對核電廠FPGA系統(tǒng)的評審過程，深入研究了FPGA系統(tǒng)的10大評審要素。研究整理出核電廠FPGA系統(tǒng)的評審導(dǎo)則和開發(fā)標(biāo)準(zhǔn)，明確了對FPGA系統(tǒng)的軟硬件雙重特性的正確認(rèn)知。
　　其次，研究了FPGA開發(fā)和驗(yàn)證的文獻(xiàn)資料，歸納出一套具有操作性的開發(fā)生命周期和V&V過程體系。該體系可以作為開發(fā)人員開展核電廠FPGA系統(tǒng)生命周期活動(dòng)的參考，并幫助監(jiān)管機(jī)構(gòu)對FPGA系統(tǒng)形成總體認(rèn)識(shí)。此套V&V方法和體系可FPGA系統(tǒng)的安全性和

3、可靠性提供充分證據(jù)。
　　再者，基于已研究的導(dǎo)則標(biāo)準(zhǔn)、開發(fā)生命周期和V&V體系，開展了基于FPGA主回路冷卻劑保護(hù)通道(PCR)開發(fā)和驗(yàn)證的研究工作。給出了開展FPGA系統(tǒng)生命周期活動(dòng)的整體框架，并突出了FPGA系統(tǒng)生命周期各項(xiàng)活動(dòng)的任務(wù)、要求和報(bào)告的組成。
　　最后，使用NuSMV語言對FPGA PCR設(shè)計(jì)建立了具體設(shè)計(jì)模型、RTL級模型和綜合級模型，并進(jìn)行形式化驗(yàn)證。模型檢驗(yàn)器NuSMV運(yùn)行時(shí)遍歷模型的所有狀態(tài)，實(shí)現(xiàn)了系

4、統(tǒng)設(shè)計(jì)模型100％覆蓋率的模型檢驗(yàn)和等價(jià)性驗(yàn)證。研究表明，形式化驗(yàn)證方法能夠有效驗(yàn)證簡單的FPGA系統(tǒng)設(shè)計(jì)。
　　本文針對核電廠FPGA系統(tǒng)的驗(yàn)證研究，探索了核電廠FPGA系統(tǒng)的開發(fā)生命周期和V&V活動(dòng)，有助于獲得具有可操作性的核電廠FPGA開發(fā)與驗(yàn)證技術(shù)，為基于FPGA的核電廠安全級儀控系統(tǒng)的V&V和評審提供理論和技術(shù)參考。此外，對形式化驗(yàn)證方法在核工業(yè)領(lǐng)域的應(yīng)用進(jìn)行了有益的探索，有助于模型檢驗(yàn)和等價(jià)性驗(yàn)證方法在核電廠儀控系統(tǒng)的