科技风
科技風
과기풍
TECHNOLOGY WIND
2012年
14期
13-16
,共4页
计算树逻辑(CTL)%程序控制流图(CFG)%代码静态分析%错误模式
計算樹邏輯(CTL)%程序控製流圖(CFG)%代碼靜態分析%錯誤模式
계산수라집(CTL)%정서공제류도(CFG)%대마정태분석%착오모식
为降低软件工程项目的开发风险和后期维护成本,本文提出一种模型检验的可扩展 C 代码静态检查方法.该方法将 C 代码常见错误归纳为可扩展的计算树逻辑公式库,同时将被检测代码转化成为程序控制流图,并将该图抽象为等价的 Kripke 结构;依据 Kripke 结构模型,使用 NuSMV工具验证公式库中的公式是否满足代码检查的要求;最后采用 GCC 编译平台提供静态检查的实验结果.该方法可以找到代码中用户事先配置的错误模式,消除代码隐患.
為降低軟件工程項目的開髮風險和後期維護成本,本文提齣一種模型檢驗的可擴展 C 代碼靜態檢查方法.該方法將 C 代碼常見錯誤歸納為可擴展的計算樹邏輯公式庫,同時將被檢測代碼轉化成為程序控製流圖,併將該圖抽象為等價的 Kripke 結構;依據 Kripke 結構模型,使用 NuSMV工具驗證公式庫中的公式是否滿足代碼檢查的要求;最後採用 GCC 編譯平檯提供靜態檢查的實驗結果.該方法可以找到代碼中用戶事先配置的錯誤模式,消除代碼隱患.
위강저연건공정항목적개발풍험화후기유호성본,본문제출일충모형검험적가확전 C 대마정태검사방법.해방법장 C 대마상견착오귀납위가확전적계산수라집공식고,동시장피검측대마전화성위정서공제류도,병장해도추상위등개적 Kripke 결구;의거 Kripke 결구모형,사용 NuSMV공구험증공식고중적공식시부만족대마검사적요구;최후채용 GCC 편역평태제공정태검사적실험결과.해방법가이조도대마중용호사선배치적착오모식,소제대마은환.
