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 条
  • [31] Navigation for Satellites
    Jacewicz, Mariusz
    Glebocki, Robert
    CHALLENGES IN AUTOMATION, ROBOTICS AND MEASUREMENT TECHNIQUES, 2016, 440 : 647 - 658
  • [32] Formal Analysis and Specification of the Triangular Format Graph
    Vose, Michael D.
    Hastings, Donald W.
    APPLIED MATHEMATICS & INFORMATION SCIENCES, 2010, 4 (01): : 15 - 30
  • [33] Analysis and Formal Specification of OpenJDK's BitSet
    Tatman, Andy S.
    Hiep, Hans-Dieter A.
    de Gouw, Stijn
    INTEGRATED FORMAL METHODS, IFM 2023, 2024, 14300 : 134 - 152
  • [34] On the Formal Specification of Regulatory Compliance: A Comparative Analysis
    Elgammal, Amal
    Turetken, Oktay
    van den Heuvel, Willem-Jan
    Papazoglou, Mike
    SERVICE-ORIENTED COMPUTING - ICSOC 2010, WORKSHOP, 2011, 6568 : 27 - 38
  • [35] Formal Specification and Analysis of Zeroconf Using Uppaal
    Berendsen, Jasper
    Gebremichael, Biniam
    Vaandrager, Frits W.
    Zhang, Miaomiao
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2011, 10 (03)
  • [36] PAFSV: A formal framework for specification and analysis of SystemVerilog
    1600, Slovak Academy of Sciences (35):
  • [37] Navigation and Annotation with Formal Concept Analysis
    Eklund, Peter
    Ducrou, Jon
    KNOWLEDGE ACQUISITION: APPROACHES, ALGORITHMS AND APPLICATIONS, 2009, 5465 : 118 - +
  • [38] A FORMAL SYSTEM FOR SPECIFICATION ANALYSIS OF CONCURRENT PROGRAMS
    HIROSE, K
    TAKAHASHI, M
    PUBLICATIONS OF THE RESEARCH INSTITUTE FOR MATHEMATICAL SCIENCES, 1983, 19 (03) : 911 - 926
  • [39] Performance analysis tools for constellations of navigation satellites
    Christophe, B
    Michal, T
    Bouchard, J
    Piet-Lahanier, H
    Flament, D
    MISSION DESIGN & IMPLEMENTATION OF SATELLITE CONSTELLATIONS, 1998, 1 : 411 - 418
  • [40] Formal Concept Analysis for Specification of Model Transformations
    Berramla, Karima
    Deba, El Abbassia
    Benyamina, A. E. H.
    Touam, Rabiaa
    Brahimi, Youcef
    Benhamamouch, Djilali
    PROCEEDINGS OF 2017 FIRST INTERNATIONAL CONFERENCE ON EMBEDDED & DISTRIBUTED SYSTEMS (EDIS 2017), 2017, : 231 - 236
12345