今日頭條
官方微信
官方抖音
案例頻道作者：北京廣利核系統(tǒng)工程有限公司 閆鑫，張智慧，任保華，齊敏
摘要：在核安全級數(shù)字化儀控系統(tǒng)中，人機交互安全控制顯示裝置的顯示內(nèi)容和控制邏輯由圖形化組態(tài)工具實現(xiàn)。由于顯示內(nèi)容規(guī)模龐大，結(jié)構(gòu)復(fù)雜，如何保證實現(xiàn)從圖形到C轉(zhuǎn)換的圖形代碼生成器（GCG）的正確性是一個難題，通過引入形式化驗證方法對GCG生成過程的正確性進行驗證。本文在對兩種形式化驗證技術(shù)比較并結(jié)合應(yīng)用場景分析之后，選取了翻譯確認(rèn)方法，并通過示例說明了方法的可行性，為之后圖形代碼生成器的形式化驗證工作奠定了基礎(chǔ)。
關(guān)鍵詞：圖形代碼生成器；形式化驗證方法；翻譯確認(rèn)；求值流圖
在線預(yù)覽：翻譯確認(rèn)方法在核安全級GCG中的應(yīng)用研究
摘自《自動化博覽》2018年4月刊
北京市公安局海淀分局備案號：11010802023656號