摄动开普勒问题形式化建模与验证  

Formal Modeling and Verification of Perturbed Kepler Problem

作　　者：王国辉 许京然[3] 刘永梅 施智平 关永[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

出　　处：《小型微型计算机系统》2020年第2期440-444,共5页Journal of Chinese Computer Systems

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

摘　　要：摄动开普勒问题广泛应用于卫星轨道摄动分析,然而卫星轨道摄动分析数学模型的错误将导致灾难性后果.传统的建模与分析方法涉及到矢量代数、旋量代数、复数、四元数等多种不同的代数系统,在各个代数系统相互转换过程中极易引入错误.几何代数方法将多种代数系统统一到相同代数结构中,弥补了传统分析方法的不足.但是基于几何代数的摄动开普勒问题数学模型的正确性并没有通过严格的形式化验证.本文采用高阶逻辑来描述该问题的属性和规范,以公认的逻辑公理和推理规则为基础构建其形式化模型并进行验证,从而最大程度确保数学模型的正确性和分析方法的可靠性.The perturbation Kepler problem is widely used in satellite orbital perturbation analysis,but some errors in the mathematical model of satellite orbit perturbation analysis will lead to catastrophic consequences. Traditional modeling and analysis methods involve many different algebraic systems,such as vector algebra,spin algebra,complex number,quaternion,etc.,and it is easy to introduce erroin the process of mutual conversion of each algebraic system. The geometric algebra method unifies a variety of algebraic systems into the same algebraic structure,making up for the shortcomings of traditional analytical methods. However,the correctness of the mathematical model of the perturbation Kepler problem based on geometric algebra has not passed the strict formal verification. In this paper,high-order logic is used to describe the attributes and norms of the problem. The formal model is constructed and verified based on the recognized logical axioms and inference rules,so as to ensure the correctness of the mathematical model and the reliability of the analytical method.

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

分 类 号：TP305[自动化与计算机技术—计算机系统结构]