计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2013年
12期
133-140
,共8页
赵岭忠%司徒凌云%翟仲毅%钱俊彦
趙嶺忠%司徒凌雲%翟仲毅%錢俊彥
조령충%사도릉운%적중의%전준언
CSP%ASP%模型检测
CSP%ASP%模型檢測
CSP%ASP%모형검측
CSP%ASP%Model checking
前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题.构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述不允许出现类环状结构的问题,可完整描述各种形态的CSP进程.研究了并发组合进程生成技术,它可使多个进程自动化并发组合,并生成一个满足所有行为特性、具有一致结构特性的新进程,保持了验证框架内进程描述的一致性,有利于并发进程的抽象与验证.实验表明了基于ASP的CSP进程描述与组合进程生成技术的有效性,以及基于该ASP描述体系的系统性质验证的可行性.
前期工作中,為解決CSP模型檢測不支持一次運行驗證多條性質的問題,構建瞭基于ASP的CSP模型檢測框架,但其存在著可描述併髮進程形態不完善與可驗證併髮繫統規模受限的問題.構建瞭全新的併髮繫統ASP描述體繫,其解決瞭前期工作中前綴描述不允許齣現類環狀結構的問題,可完整描述各種形態的CSP進程.研究瞭併髮組閤進程生成技術,它可使多箇進程自動化併髮組閤,併生成一箇滿足所有行為特性、具有一緻結構特性的新進程,保持瞭驗證框架內進程描述的一緻性,有利于併髮進程的抽象與驗證.實驗錶明瞭基于ASP的CSP進程描述與組閤進程生成技術的有效性,以及基于該ASP描述體繫的繫統性質驗證的可行性.
전기공작중,위해결CSP모형검측불지지일차운행험증다조성질적문제,구건료기우ASP적CSP모형검측광가,단기존재착가묘술병발진정형태불완선여가험증병발계통규모수한적문제.구건료전신적병발계통ASP묘술체계,기해결료전기공작중전철묘술불윤허출현류배상결구적문제,가완정묘술각충형태적CSP진정.연구료병발조합진정생성기술,타가사다개진정자동화병발조합,병생성일개만족소유행위특성、구유일치결구특성적신진정,보지료험증광가내진정묘술적일치성,유리우병발진정적추상여험증.실험표명료기우ASP적CSP진정묘술여조합진정생성기술적유효성,이급기우해ASP묘술체계적계통성질험증적가행성.
