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