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

摘要

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