计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
z1期
77-86,111
,共11页
侯刚%周宽久%勇嘉伟%任龙涛%王小龙
侯剛%週寬久%勇嘉偉%任龍濤%王小龍
후강%주관구%용가위%임룡도%왕소룡
软件系统%模型检测%状态空间爆炸%形式化验证
軟件繫統%模型檢測%狀態空間爆炸%形式化驗證
연건계통%모형검측%상태공간폭작%형식화험증
Software systems%Model checking%State explosion%Formal verification
模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题.如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题.系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向.
模型檢測已成為保證軟件繫統正確性和可靠性的重要手段,但隨著軟件功能日益彊大,其規模和複雜度也越來越大,在模型檢測過程中容易產生狀態爆炸問題.如何解決模型檢測中的狀態爆炸,已成為工業界和理論界無法迴避的重要課題.繫統地綜述模型檢測領域解決狀態爆炸問題的關鍵技術和主要方法,併提齣該領域的最新研究進展與方嚮.
모형검측이성위보증연건계통정학성화가고성적중요수단,단수착연건공능일익강대,기규모화복잡도야월래월대,재모형검측과정중용역산생상태폭작문제.여하해결모형검측중적상태폭작,이성위공업계화이론계무법회피적중요과제.계통지종술모형검측영역해결상태폭작문제적관건기술화주요방법,병제출해영역적최신연구진전여방향.
