摘 要：文章主要以雷达系统软件安全为背景，首先提出了从 C 程序到基于一阶逻辑的形式模型的总体转换方法，通过定义辅助运算子，给出从 C 程序到形式模型保持语义一致的映射规则，对 C 程序的核心结构如赋值语句、条件语句、循环语句以及函数结构进行了规约，从而得到可执行的形式模型。最后，给出一个典型的 C 程序案例，应用转换规则生成了对应的形式模型，验证了转换方法的有效性。
关键词：软件安全；C 程序；一阶逻辑；形式模型
DOI:10.19850/j.cnki.2096-4706.2022.07.006
中图分类号：TP311.5 文献标识码：A 文章编号：2096-4706（2022）07-0026-04
A Conversion Method of C Program to Formal Model Based on Radar Software Security
ZANG Weiwang, ZHU Jian
(Nanjing Research Institute of Electronics Technology, Nanjing 210039, China)
Abstract: 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.
Keywords: software security; C program; first-order logic; formal model
参考文献：
[1] 朱亚伟，左志强，王林章，等 .C 程序内存泄漏智能化检测方法 [J]. 软件学报，2019，30（5）：1330-1341.
[2] 张广泉 . 形式化方法导论 [M]. 北京：清华大学出版社，2015
[3] 朱健，胡凯，张伯钧 . 智能合约的形式化验证方法研究综述 [J]. 电子学报，2021，49（4）：792-804.
[4] 张石生，向淑文 .Brouwer 不动点定理的等价形式 [J]. 纯粹数学与应用数学，1991（2）：27-31.
[5] 王明文，孙永强 . 对象式 Lam bda 演算的自作用部分计值 [J]. 软件学报，2001（8）：1154-1161.
[6] ABRIAL J. Modelling in Event-B：System and Software Engineering [M].UK：Cambridge University Press，2009.
[7] MEDIAWIKI. Rodin platform [EB/OL].（2021-12-01）.http://wiki.Event-B.org/index.php/Rodin_Platform.
作者简介：臧伟旺（1982—），男，汉族，河南汤阴人，高级工程师，硕士，研究方向：机载火控雷达和导引头雷达系统论证；朱健（1997—），男，汉族，安徽铜陵人，助理工程师，硕士，研究方向：形式化方法与导引头雷达设计。