题目：导航星座可用性度量与仿真评价研究

随着航空航天技术的不断进步，以及信息化产业的不断发展，人们对于卫星的依赖越来越强，卫星导航技术的应用已经渗透到人们日常的生活中。卫星导航技术不仅关系着人们物质条件的满足，并且关系着国家的国防建设，以及国家的综合国力。如今，从日常的人们车载导航工具的定位，到民航的航班的飞行定位，从战斗机的高速巡航到舰船的海事活动已经都离不开导航卫星的支持。所以导航卫星的可用性已经关系到国家的军事活动的安全和人们的生活质量。

如何对导航卫星的设计以及星座体系的配置进行评估，使其能够满足导航要求，是本文研究的一个基本出发点。用户对于导航卫星的使用，更多的是关注导航的可用性，地面控制系统的可靠性、卫星的可靠性和星座的配置都会对导航的可用性产生影响。因此本文首先对导航系统的可用性的度量体系进行分解，然后通过建模方法分别对单星、星座、以及用户导航星座的可用性进行了建模，同时利用模型检查对可用性进行了定量的评价。本文的主要研究内容有：

（1）    卫星导航系统相关分析

对现有的导航系统的组成做了介绍，同时针对系统的特点，分析了系统的故障模式，把系统的故障模式分为四部分，分别是硬失效、耗损失效、软失效和卫星运行与维护操作。最后，民航对导航系统的需求做了分析。

（2）    导航系统的参数分析

给出了导航信号健康的概念，以及顶层参数，精确性，可用性，完好性，连续性的概念。接着根据顶层参数的概念，分析四大参数之间的关系，提出了顶层参数关系U型模型。构建了构建导航系统的可用性度量体系，导航系统的可用性度量体系有三部分组成，分别是导航信号测量指标体系、星座覆盖性度量体系和星座可用性度量体系。（3）    单星可用性度量方法研究

介绍了形式化分析方法，分析了形式化方法与传统方法的不同，针对单星的系统的特点，建立了单星系统的可用性模型，通过模型检查方法对导航系统的可用性属性做了定量分析，分析了可靠性，维修性对单星可用性的影响。

（4）    星座系统可用性度量方法研究

分析了星座系统的运行方式，建立了星座系统的形式化模型，通过模型检查，定量分析了导航星座系统的可用性属性，分析了可靠性，维修性对星座系统的可用性的影响。

（5）    导航可用性度量方法研究

对导航星座系统做了介绍，通过一个航班的例子，构建了导航可用性系统模型。介绍了π演算的基本定义与语义，并对导航可用性各个系统进行了π演算的描述。最后把π演算转化成能够定量分析的CTMC模型，对模型进行模型检查分析，得到导航可用性。