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