企业简介

  • 公司类型：供应商

联系方式
  • 北京广利核系统工程有限公司
  • 地址：海淀区农大南路1号硅谷亮城9号楼
  • 邮编：100084
  • 电话：010-62667237
  • 传真：010-62667199
  • 网址：http://www.ctecdcs.com
  • Email：chenhongyu@hollysys.com
  • 联系人：
案例详细
标题可信编译器中地址不相交的保持性证明
技术领域工业安全
行业
简介同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言，在同步数据流语言到顺序执行语言的翻译转换过程中，语义等价要保证赋值语句的左右值地址互不相交，这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质，并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。
内容

北京广利核系统工程有限公司 谷伟卿，张智慧，白涛，齐敏

摘要：同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言，在同步数据流语言到顺序执行语言的翻译转换过程中，语义等价要保证赋值语句的左右值地址互不相交，这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质，并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。

关键词：同步数据流；定理证明；Coq；语义等价；地址不相交

在线预览：可信编译器中地址不相交的保持性证明

摘自《自动化博览》2017年4月刊