基于雷达软件安全的C程序到形式模型的转换方法

摘要：

文章主要以雷达系统软件安全为背景,首先提出了从C程序到基于一阶逻辑的形式模型的总体转换方法,通过定义辅助运算子,给出从C程序到形式模型保持语义一致的映射规则,对C程序的核心结构如赋值语句、条件语句、循环语句以及函数结构进行了规约,从而得到可执行的形式模型.最后,给出一个典型的C程序案例,应用转换规则生成了对应的形式模型,验证了转换方法的有效性.

关键词：软件安全、C程序、一阶逻辑、形式模型

所属期刊栏目：6

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

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

页数：共4页

页码：26-28,31