西安交通大学学报
西安交通大學學報
서안교통대학학보
JOURNAL OF XI'AN JIAOTONG UNIVERSITY
2006年
4期
377-380
,共4页
肖健宇%张德运%郑卫斌%张勇
肖健宇%張德運%鄭衛斌%張勇
초건우%장덕운%정위빈%장용
程序条件化%软件模型检测%状态空间缩减%符号化执行%线性时序逻辑
程序條件化%軟件模型檢測%狀態空間縮減%符號化執行%線性時序邏輯
정서조건화%연건모형검측%상태공간축감%부호화집행%선성시서라집
针对软件模型检测中的状态爆炸问题,提出将程序条件化技术用于软件状态空间缩减的方案.以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件,通过分析程序符号化执行语义,借助自动定理证明器,对语句的可达性条件进行逻辑推理,删除那些与性质的可满足性无关的语句,以达到程序精简的目的.理论分析和实验结果表明,条件化可以有效缩减程序状态空间,而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息,满足软件模型检测对状态缩减的安全性要求.
針對軟件模型檢測中的狀態爆炸問題,提齣將程序條件化技術用于軟件狀態空間縮減的方案.以程序性質的線性時序邏輯公式可能齣現的蘊涵式的前件作為條件化的約束條件,通過分析程序符號化執行語義,藉助自動定理證明器,對語句的可達性條件進行邏輯推理,刪除那些與性質的可滿足性無關的語句,以達到程序精簡的目的.理論分析和實驗結果錶明,條件化可以有效縮減程序狀態空間,而且縮減後的程序模型保留瞭原程序中與所需驗證的性質有關的所有信息,滿足軟件模型檢測對狀態縮減的安全性要求.
침대연건모형검측중적상태폭작문제,제출장정서조건화기술용우연건상태공간축감적방안.이정서성질적선성시서라집공식가능출현적온함식적전건작위조건화적약속조건,통과분석정서부호화집행어의,차조자동정리증명기,대어구적가체성조건진행라집추리,산제나사여성질적가만족성무관적어구,이체도정서정간적목적.이론분석화실험결과표명,조건화가이유효축감정서상태공간,이차축감후적정서모형보류료원정서중여소수험증적성질유관적소유신식,만족연건모형검측대상태축감적안전성요구.
