今日头条
官方微信
官方抖音
案例频道作者：北京广利核系统工程有限公司 闫鑫，张智慧，任保华，齐敏
摘要：在核安全级数字化仪控系统中，人机交互安全控制显示装置的显示内容和控制逻辑由图形化组态工具实现。由于显示内容规模庞大，结构复杂，如何保证实现从图形到C转换的图形代码生成器（GCG）的正确性是一个难题，通过引入形式化验证方法对GCG生成过程的正确性进行验证。本文在对两种形式化验证技术比较并结合应用场景分析之后，选取了翻译确认方法，并通过示例说明了方法的可行性，为之后图形代码生成器的形式化验证工作奠定了基础。
关键词：图形代码生成器；形式化验证方法；翻译确认；求值流图
在线预览：翻译确认方法在核安全级GCG中的应用研究
摘自《自动化博览》2018年4月刊
北京市公安局海淀分局备案号：11010802023656号