四川理工学院学报（自然科学版）
四川理工學院學報（自然科學版）
사천리공학원학보（자연과학판）
Journal of Sichuan University of Science & Engineering(Natural Sicence Edition)
2015年
5期
51-56
,共6页
Lebesgue积分%PVS%形式化%反相积分器
Lebesgue積分%PVS%形式化%反相積分器
Lebesgue적분%PVS%형식화%반상적분기
针对传统模型验证方法存在效率低和模型较为复杂的缺点,将Lebesgue积分的运算特征引入模型验证和测试,提出一种基于Lebesgue积分的形式化验证和测试方法.通过不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则以及极限定理等方面的形式化,实现Lebesgue积分的运算特征在PVS(Prototype Verification System)定理证明器中的形式化.以标准反相积分器为应用模型验证数学理论和公式推导的正确性,通过数理分析验证Lebesgue积分形式化定理库在计算机信息安全领域应用的正确性.测试结果证明了Lebesgue积分在PVS中进行形式化的可行性和有效性.
針對傳統模型驗證方法存在效率低和模型較為複雜的缺點,將Lebesgue積分的運算特徵引入模型驗證和測試,提齣一種基于Lebesgue積分的形式化驗證和測試方法.通過不等式計算、閉區間子集可積分性、多重分部、線性運算、Cauchy可積分準則以及極限定理等方麵的形式化,實現Lebesgue積分的運算特徵在PVS(Prototype Verification System)定理證明器中的形式化.以標準反相積分器為應用模型驗證數學理論和公式推導的正確性,通過數理分析驗證Lebesgue積分形式化定理庫在計算機信息安全領域應用的正確性.測試結果證明瞭Lebesgue積分在PVS中進行形式化的可行性和有效性.
침대전통모형험증방법존재효솔저화모형교위복잡적결점,장Lebesgue적분적운산특정인입모형험증화측시,제출일충기우Lebesgue적분적형식화험증화측시방법.통과불등식계산、폐구간자집가적분성、다중분부、선성운산、Cauchy가적분준칙이급겁한정리등방면적형식화,실현Lebesgue적분적운산특정재PVS(Prototype Verification System)정리증명기중적형식화.이표준반상적분기위응용모형험증수학이론화공식추도적정학성,통과수리분석험증Lebesgue적분형식화정리고재계산궤신식안전영역응용적정학성.측시결과증명료Lebesgue적분재PVS중진행형식화적가행성화유효성.
