文献类型：期刊文章

作　　者：王国辉[1,2] 许京然[3] 刘永梅[1,4] 施智平[2,4] 关永[1,4]

WANG Guo-hui;XU Jing-ran;LIU Yong-mei;SHI Zhi-ping;GUAN Yong(Beijing Key Laboratory of Electronic System Reliability and Prognostics.College of Information and Engineering,Capital Normal University,Beijing 100048,China;Beijing Advanced Innovation Center for Theory and Imaging Technology,Capital Normal University,Beijing 100048,China;Department of Informatics.Beijing City University,Beijing 101399,China;International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary,Capital Normal University,Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,电子系统可靠性技术北京市重点实验室,北京100048 [2]首都师范大学北京成像理论与技术高精尖创新中心,100048 [3]北京城市学院信息学部,北京101399 [4]首都师范大学电子系统可靠性与数理交叉学科国家国际科技合作示范型基地,北京100048

出　　处：《小型微型计算机系统》

基　　金：国家重点研发计划项目(2017YFB1302800)资助;国家自然科学基金项目(61876111,61572331,61602325,61877040)资助;科技创新服务能力建设-基本科研业务费(科研类)项目(025185305000)资助.

年　　份：2020

卷　　号：41

期　　号：2

起止页码：440-444

语　　种：中文

收录情况：AJ、BDHX、BDHX2017、CSA、CSA-PROQEUST、CSCD、CSCD_E2019_2020、IC、INSPEC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：摄动开普勒问题广泛应用于卫星轨道摄动分析,然而卫星轨道摄动分析数学模型的错误将导致灾难性后果.传统的建模与分析方法涉及到矢量代数、旋量代数、复数、四元数等多种不同的代数系统,在各个代数系统相互转换过程中极易引入错误.几何代数方法将多种代数系统统一到相同代数结构中,弥补了传统分析方法的不足.但是基于几何代数的摄动开普勒问题数学模型的正确性并没有通过严格的形式化验证.本文采用高阶逻辑来描述该问题的属性和规范,以公认的逻辑公理和推理规则为基础构建其形式化模型并进行验证,从而最大程度确保数学模型的正确性和分析方法的可靠性.

关 键 词：形式化验证 定理证明 几何代数 摄动 卫星轨道

分 类 号：TP305]