同步语言多线程代码生成的语义保持证明方法

摘要：

同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋势,同步语言的多线程代码生成及其语义保持证明研究成为研究热点.目前,已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明.因此,本文提出一种同步语言SIGNAL多线程代码生成的语义保持证明方法:首先形式化定义编译过程中源、目标、中间语言的结构化操作语义;其次形式化定义多线程代码生成过程;最后基于互模拟等价思想证明编译前后的语义一致性.

关键词：同步语言、安全关键软件、多任务代码生成、语义保持证明、Coq

所属期刊栏目：43

分类号：TP311(计算技术、计算机技术)

资助基金：本课题得到国家自然科学基金;航空科学基金;GF基础科研重点项目;中央高校基本科研业务费专项资金资助;南京航空航天大学研究生创新基地实验室开放基金

在线出版日期：2020-11-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：2216-2226