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

打开文本图片集

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

网站仅支持在线阅读（不支持PDF下载），如需保存文章，可以选择【打印】保存。