计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2015年
8期
2387-2390,2394
,共5页
模型检测%状态空间爆炸%软件测试%LOTOS%μ-演算
模型檢測%狀態空間爆炸%軟件測試%LOTOS%μ-縯算
모형검측%상태공간폭작%연건측시%LOTOS%μ-연산
model checking%state space explosion%software testing%LOTOS%μ-calculus
为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法.该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储;然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换,再利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述;最后使用模型检测工具验证被测程序是否满足测试目的.实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测,并且可以缓解状态空间爆炸问题.
為瞭實現對偽代碼的模型檢測併且能夠緩解模型檢測中的狀態空間爆炸問題,提齣瞭測試目的引導的模型檢測方法.該方法的基本思想是首先對偽代碼進行模塊劃分併對每箇模塊進行建模,穫取基本路徑的集閤併以流圖的方式進行存儲;然後利用自主開髮的轉換工具實現流圖到國際標準語言LOTOS的轉換,再利用自主開髮的輔助工具μ-縯算編輯器對測試目的進行描述;最後使用模型檢測工具驗證被測程序是否滿足測試目的.實驗結果錶明,測試目的引導的模型檢測方法能夠實現對偽代碼的模型檢測,併且可以緩解狀態空間爆炸問題.
위료실현대위대마적모형검측병차능구완해모형검측중적상태공간폭작문제,제출료측시목적인도적모형검측방법.해방법적기본사상시수선대위대마진행모괴화분병대매개모괴진행건모,획취기본로경적집합병이류도적방식진행존저;연후이용자주개발적전환공구실현류도도국제표준어언LOTOS적전환,재이용자주개발적보조공구μ-연산편집기대측시목적진행묘술;최후사용모형검측공구험증피측정서시부만족측시목적.실험결과표명,측시목적인도적모형검측방법능구실현대위대마적모형검측,병차가이완해상태공간폭작문제.
