计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2008年
27期
46-48,64
,共4页
符号模型检验%吴方法%特征列
符號模型檢驗%吳方法%特徵列
부호모형검험%오방법%특정렬
模型检验技术广泛应用于验证并发系统的性质.它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题.然而,随着系统规模的增大,BDD的大小仍呈指数增长.吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明.给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题.
模型檢驗技術廣汎應用于驗證併髮繫統的性質.它的瓶頸一直是內存爆炸問題,將BDD技術引入到模型檢驗中的方法能有效地緩和狀態組閤爆炸問題.然而,隨著繫統規模的增大,BDD的大小仍呈指數增長.吳方法是一種處理多項式的符號計算方法,能有效地求解代數方程組併成功地應用于幾何定理機器證明.給齣應用吳方法計算錶示Kripke結構和CTL公式的多項式的特徵列的方法,從而實現對較大規模的繫統性質的驗證,進一步緩和狀態組閤爆炸問題.
모형검험기술엄범응용우험증병발계통적성질.타적병경일직시내존폭작문제,장BDD기술인입도모형검험중적방법능유효지완화상태조합폭작문제.연이,수착계통규모적증대,BDD적대소잉정지수증장.오방법시일충처리다항식적부호계산방법,능유효지구해대수방정조병성공지응용우궤하정리궤기증명.급출응용오방법계산표시Kripke결구화CTL공식적다항식적특정렬적방법,종이실현대교대규모적계통성질적험증,진일보완화상태조합폭작문제.
