基于模式识别的Lebesgue积分在PVS中的形式化证明与分析

• 作者: 张少芳 李冀东
• 来源期刊: 四川理工学院学报（自然科学版）
• 学科: 工学
• 关键词: Lebesgue积分 PVS 形式化 反相积分器
• 年，卷（期）: 2015,（5）
• 所属期刊栏目: 机械、电子及计算机科学
• 页码范围: 51-56
• 页数: 6页
• 分类号: TP391
• 字数: 2620字
• 语种: 中文
• DOI: 10.11863/j.suse.2015.05.10

摘要

针对传统模型验证方法存在效率低和模型较为复杂的缺点,将Lebesgue积分的运算特征引入模型验证和测试,提出一种基于Lebesgue积分的形式化验证和测试方法.通过不等式计算、闭区间子集可积分性、多重分部、线性运算、Cauchy可积分准则以及极限定理等方面的形式化,实现Lebesgue积分的运算特征在PVS(Prototype Verification System)定理证明器中的形式化.以标准反相积分器为应用模型验证数学理论和公式推导的正确性,通过数理分析验证Lebesgue积分形式化定理库在计算机信息安全领域应用的正确性.测试结果证明了Lebesgue积分在PVS中进行形式化的可行性和有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张少芳		46	34	3.0	4.0
2	李冀东		21	29	3.0	4.0