基于雷達軟件安全的C程序到形式模型的轉(zhuǎn)換方法

打開文本圖片集

摘  要：文章主要以雷達系統(tǒng)軟件安全為背景，首先提出了從C程序到基于一階邏輯的形式模型的總體轉(zhuǎn)換方法，通過定義輔助運算子，給出從C程序到形式模型保持語義一致的映射規(guī)則，對C程序的核心結(jié)構(gòu)如賦值語句、條件語句、循環(huán)語句以及函數(shù)結(jié)構(gòu)進行了規(guī)約，從而得到可執(zhí)行的形式模型。最后，給出一個典型的C程序案例，應(yīng)用轉(zhuǎn)換規(guī)則生成了對應(yīng)的形式模型，驗證了轉(zhuǎn)換方法的有效性。（剩余5862字）