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 条
  • [21] THE NAVIGATION OF NAVIGATION SATELLITES
    ASHKENAZI, V
    MOORE, T
    JOURNAL OF NAVIGATION, 1986, 39 (03): : 377 - 393
  • [22] Risk of collisions for constellation satellites
    A. Rossi
    G. B. Valsecchi
    P. Farinella
    Nature, 1999, 399 : 743 - 743
  • [23] Risk of collisions for constellation satellites
    Rossi, A
    Valsecchi, GB
    Farinella, P
    NATURE, 1999, 399 (6738) : 743 - 744
  • [24] Comparative Analysis of Secure QKD Protocols for Small Satellites Constellation
    Kaur, Hardeer
    Singh, Jai Sukh Paul
    COMPUTER AIDED CONSTELLATION MANAGEMENT AND COMMUNICATION SATELLITES, ICSS 2022, 2023, 987 : 185 - 200
  • [25] A modeling-based approach for dependability analysis of a constellation of satellites
    Farias, Daniel
    Nogueira, Bruno
    Farias Junior, Ivaldir
    Andrade, Ermeson
    SOFTWARE AND SYSTEMS MODELING, 2025, 24 (01): : 209 - 224
  • [26] Combining formal specification methods and informal specification methods for requirement analysis
    Zhang, LC
    1997 IEEE PACIFIC RIM CONFERENCE ON COMMUNICATIONS, COMPUTERS AND SIGNAL PROCESSING, VOLS 1 AND 2: PACRIM 10 YEARS - 1987-1997, 1997, : 444 - 447
  • [27] Spacecrafts Navigation Demand Analysis and Simulation on MEO Constellation
    Li, Peng
    Chen, Zhonggui
    Wu, Xiangjun
    Hao, Wenyu
    Wang, Lu
    CHINA SATELLITE NAVIGATION CONFERENCE (CSNC) 2016 PROCEEDINGS, VOL I, 2016, 388 : 241 - 255
  • [28] Analysis of the timing system error of the constellation automatic navigation
    Lu Xiaochun
    Wu Haitao
    Li Xiaohui
    Chen Xiaozhong
    PROCEEDINGS OF THE 2007 IEEE INTERNATIONAL FREQUENCY CONTROL SYMPOSIUM-JOINTLY WITH THE 21ST EUROPEAN FREQUENCY AND TIME FORUM, VOLS 1-4, 2007, : 279 - +
  • [29] FORMAL SPECIFICATION
    BROKATE, K
    COMPUTER JOURNAL, 1988, 31 (02): : 190 - 190
  • [30] NAVIGATION SATELLITES
    不详
    SPACEFLIGHT, 1966, 8 (02): : 60 - &
12345