计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2012年
6期
47-49
,共3页
错误模式%模型检验%CTL公式%控制流图%Kripke结构%CoSy编译器平台
錯誤模式%模型檢驗%CTL公式%控製流圖%Kripke結構%CoSy編譯器平檯
착오모식%모형검험%CTL공식%공제류도%Kripke결구%CoSy편역기평태
为提高程序编写的正确率,减少软件开发和维护开销,提出一种基于错误模式和模型检验的静态代码分析方法.该方法将C语言程序常见的错误模式以CTL公式表示,形成可扩展的CTL公式库,生成待检测程序的控制流图(CFG)后,将CFG抽象并转化为等价的Kripke结构,利用标号算法实现模型检验,由此验证程序的正确性.基于CoSy编译平台的实验结果表明,该方法能正确查找出程序中存在的错误模式,且具有良好的可扩展性.
為提高程序編寫的正確率,減少軟件開髮和維護開銷,提齣一種基于錯誤模式和模型檢驗的靜態代碼分析方法.該方法將C語言程序常見的錯誤模式以CTL公式錶示,形成可擴展的CTL公式庫,生成待檢測程序的控製流圖(CFG)後,將CFG抽象併轉化為等價的Kripke結構,利用標號算法實現模型檢驗,由此驗證程序的正確性.基于CoSy編譯平檯的實驗結果錶明,該方法能正確查找齣程序中存在的錯誤模式,且具有良好的可擴展性.
위제고정서편사적정학솔,감소연건개발화유호개소,제출일충기우착오모식화모형검험적정태대마분석방법.해방법장C어언정서상견적착오모식이CTL공식표시,형성가확전적CTL공식고,생성대검측정서적공제류도(CFG)후,장CFG추상병전화위등개적Kripke결구,이용표호산법실현모형검험,유차험증정서적정학성.기우CoSy편역평태적실험결과표명,해방법능정학사조출정서중존재적착오모식,차구유량호적가확전성.
