计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2006年
19期
51-53
,共3页
肖健宇%张德运%陈海诠%董皓
肖健宇%張德運%陳海詮%董皓
초건우%장덕운%진해전%동호
软件模型检测%状态-迁移模型%状态爆炸%程序条件化%自动定理证明
軟件模型檢測%狀態-遷移模型%狀態爆炸%程序條件化%自動定理證明
연건모형검측%상태-천이모형%상태폭작%정서조건화%자동정리증명
提出用条件化技术对程序进行预处理的方案,以克服软件模型检测中状态空间爆炸问题.以程序性质公式中蕴涵式的前件作为约束条件,通过对程序符号化执行后各控制点的路径条件进行逻辑推理,删除那些对性质检测无关的语句.理论分析和实验结果表明,条件化可以有效缩减程序状态空间,并且满足软件模型检测对状态缩减的安全性要求.
提齣用條件化技術對程序進行預處理的方案,以剋服軟件模型檢測中狀態空間爆炸問題.以程序性質公式中蘊涵式的前件作為約束條件,通過對程序符號化執行後各控製點的路徑條件進行邏輯推理,刪除那些對性質檢測無關的語句.理論分析和實驗結果錶明,條件化可以有效縮減程序狀態空間,併且滿足軟件模型檢測對狀態縮減的安全性要求.
제출용조건화기술대정서진행예처리적방안,이극복연건모형검측중상태공간폭작문제.이정서성질공식중온함식적전건작위약속조건,통과대정서부호화집행후각공제점적로경조건진행라집추리,산제나사대성질검측무관적어구.이론분석화실험결과표명,조건화가이유효축감정서상태공간,병차만족연건모형검측대상태축감적안전성요구.
