Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites

被引：7
|
作者：
Peng, Zhaoguang [1 ,3 ]
Lu, Yu [2 ]
Miller, Alice [2 ]
Zhao, Tingdi [3 ]
Johnson, Chris [2 ]
机构：
[1] China Ceprei Lab, Guangzhou, Guangdong, Peoples R China
[2] Univ Glasgow, Sch Comp Sci, Glasgow G12 8RZ, Lanark, Scotland
[3] Beijing Univ Aeronaut & Astronaut, Sch Reliabil & Syst Engn, Beijing 100083, Peoples R China
来源：
QUALITY AND RELIABILITY ENGINEERING INTERNATIONAL | 2016年 / 32卷 / 02期
关键词：
navigation satellite systems; reliability; availability; maintainability; probabilistic model checking; SYMBOLIC MODEL CHECKING;
D O I：
10.1002/qre.1754
中图分类号：
T [工业技术];
学科分类号：
08 ;
摘要：
Navigation satellites are a core component of navigation satellite-based systems such as Global Positioning System, Global Navigation Satellite System and Galileo, which provide location and timing information for a variety of uses. Such satellites are designed for operating on orbit to perform tasks and have lifetimes of 10years or more. Reliability, availability and maintainability analysis of systems has been indispensable in the design phase of satellites in order to achieve minimum failures or to increase mean time between failures and thus to plan maintenance strategies, optimise reliability and maximise availability. In this paper, we present formal models of both a single satellite and a navigation satellite constellation and logical specification of their reliability, availability and maintainability properties, respectively. The probabilistic model checker PRISM has been used to perform automated analysis of these quantitative properties. Copyright (c) 2014 John Wiley & Sons, Ltd.
引用
收藏
页码：345 / 361
页数：17
相关论文
共 50 条
  • [41] FAUST: Formal analysis using specification tools
    Rifaut, A
    Massonet, P
    Molderez, JF
    Ponsard, C
    Stadnik, P
    van Lamsweerde, A
    Van Hung, T
    11TH IEEE INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 350 - 350
  • [42] INTEGRATED STRUCTURED ANALYSIS AND FORMAL SPECIFICATION TECHNIQUES
    SEMMENS, LT
    FRANCE, RB
    DOCKER, TWG
    COMPUTER JOURNAL, 1992, 35 (06): : 600 - 610
  • [43] PAFSV: A FORMAL FRAMEWORK FOR SPECIFICATION AND ANALYSIS OF SYSTEMVERILOG
    Man, Ka Lok
    Lei, Chi-Un
    Kapoor, Hemangee K.
    Krilavicius, Tomas
    Ma, Jieming
    Zhang, Nan
    COMPUTING AND INFORMATICS, 2016, 35 (01) : 143 - 176
  • [44] Analysis of Sun Outage Influence on Navigation Constellation Crosslink
    Xu, Zhiqian
    Yang, Jun
    Zhang, Chuansheng
    Chen, Jianyun
    CSNC 2011: 2ND CHINA SATELLITE NAVIGATION CONFERENCE, VOLS 1-3, 2011, : 1200 - 1203
  • [45] Analysis and Simulation on the Characteristic of Navigation Constellation Crosslink GDOP
    Chen, Jianyun
    Xu, Bo
    Zhou, Yongbin
    Zhang, Chuansheng
    CSNC 2011: 2ND CHINA SATELLITE NAVIGATION CONFERENCE, VOLS 1-3, 2011, : 394 - 398
  • [46] Research on formal security policy model specification and its formal analysis
    Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
    不详
    不详
    Tongxin Xuebao, 2006, 6 (94-101):
  • [47] Design and simulation of regional navigation constellation with optimized mean DOP based on hybrid GEO and IGSO satellites
    Keyvani F.
    Torabi S.H.
    International Journal of Aviation, Aeronautics, and Aerospace, 2019, 6 (02):
  • [48] Ka-Band Inter-Satellite Link System Design for MEO Navigation Satellites Constellation
    Chakraborty, Sucharita
    Bhadouria, Vijay
    Upadhyay, Dhaval
    Bera, Subhash Chandra
    2024 INTERNATIONAL CONFERENCE ON SIGNAL PROCESSING AND COMMUNICATIONS, SPCOM 2024, 2024,
  • [49] Design and Simulation of Regional Navigation Constellation with Optimized Mean DOP based on Hybrid GEO and IGSO Satellites
    Keyvani, Firooz
    Torabi, Seyed Hosein
    INTERNATIONAL JOURNAL OF AVIATION AERONAUTICS AND AEROSPACE, 2019, 6 (02):
  • [50] Performance Analysis for Bearings-only Geolocation Based on Constellation of Satellites
    Li, Jinzhou
    Lv, Shouye
    Yang, Liu
    Wu, Sheng
    Liu, Yang
    Luan, Qijun
    2022 IEEE INTERNATIONAL CONFERENCE ON TRUST, SECURITY AND PRIVACY IN COMPUTING AND COMMUNICATIONS, TRUSTCOM, 2022, : 1429 - 1434
12345