计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2011年
4期
295-298
,共4页
庞征斌%屈婉霞%郭阳%杨晓东
龐徵斌%屈婉霞%郭暘%楊曉東
방정빈%굴완하%곽양%양효동
参数化系统验证%二维抽象%模拟%性质保持
參數化繫統驗證%二維抽象%模擬%性質保持
삼수화계통험증%이유추상%모의%성질보지
模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件,参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象,证明了此抽象方法的正确性和合理性,即TDA模型与原始模型存在模拟关系,而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式,在任意规模的原始模型中也成立,为简化参数化系统验证提供了理论依据.
模型之間的等價關繫和抽象模型的性質保持是保證驗證正確的必要條件,參數化繫統二維抽象從構成繫統狀態空間的二維方嚮分彆進行抽象,證明瞭此抽象方法的正確性和閤理性,即TDA模型與原始模型存在模擬關繫,而且在TDA模型中成立的隻對單箇變量進行全稱量化的單索引ACTL*公式,在任意規模的原始模型中也成立,為簡化參數化繫統驗證提供瞭理論依據.
모형지간적등개관계화추상모형적성질보지시보증험증정학적필요조건,삼수화계통이유추상종구성계통상태공간적이유방향분별진행추상,증명료차추상방법적정학성화합이성,즉TDA모형여원시모형존재모의관계,이차재TDA모형중성립적지대단개변량진행전칭양화적단색인ACTL*공식,재임의규모적원시모형중야성립,위간화삼수화계통험증제공료이론의거.
