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

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

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

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

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