导航卫星星座的形式化规范与定量分析
系统与控制
2014-10-24 v5
摘要
导航卫星是基于导航卫星系统（如 GPS、GLONASS 和 Galileo）的核心组件，这些系统为各种用途提供位置和计时信息。此类卫星设计用于在轨运行以执行任务，寿命可达 10 年或更长。在卫星设计阶段，系统的可靠性、可用性和可维护性 (RAM) 分析对于实现最小化故障、增加平均故障间隔时间 (MTBF)、规划维护策略、优化可靠性以及最大化可用性至关重要。本文提出了单颗卫星和导航卫星星座的形式化模型，并分别对其可靠性、可用性和可维护性属性进行了逻辑规范。我们使用概率模型检测器 PRISM 对这些定量属性进行了自动化分析。
引用
@article{arxiv.1402.5599,
title = {Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites},
author = {Zhaoguang Peng and Yu Lu and Alice Miller and Tingdi Zhao and Chris Johnson},
journal= {arXiv preprint arXiv:1402.5599},
year = {2014}
}