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

A Conversion Method of C Program to Formal Model Based on Radar Software Security

作　　者：臧伟旺[1] 朱健 ZANG Weiwang;ZHU Jian(Nanjing Research Institute of Electronics Technology,Nanjing 210039,China)

机构地区：[1]南京电子技术研究所,江苏南京210039

出　　处：《现代信息科技》2022年第7期26-28,31,共4页Modern Information Technology

摘　　要：文章主要以雷达系统软件安全为背景,首先提出了从C程序到基于一阶逻辑的形式模型的总体转换方法,通过定义辅助运算子,给出从C程序到形式模型保持语义一致的映射规则,对C程序的核心结构如赋值语句、条件语句、循环语句以及函数结构进行了规约,从而得到可执行的形式模型。最后,给出一个典型的C程序案例,应用转换规则生成了对应的形式模型,验证了转换方法的有效性。This paper mainly takes the software security of radar system as the background,firstly proposes a general conversion method from C program to formal model based on first-order logic,and gives the mapping rules from C program to formal model to maintain semantic consistency by defining auxiliary operators.The core structures of C programs such as assignment statements,conditional statements,loop statements and function structures are specified,so as to obtain an executable formal model.Finally,a typical C program case is given,and the corresponding formal model is generated by applying the transformation rules,which verifies the validity of the transformation method.

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]