A Probabilistic Model Checking Approach to Analysing Reliability, Availability, and Maintainability of a Single Satellite System

Author

Zhaoguang Peng ; Yu Lu ; Miller, Alice ; Johnson, Chris ; Tingdi Zhao

Author_Institution

Sch. of Reliability & Syst. Eng., Beijing Univ. of Aeronaut. & Astronaut., Beijing, China

fYear

2013

Firstpage

611

Lastpage

616

Abstract

Satellites now form a core component for space based systems such as GPS and GLONAS which provide location and timing information for a variety of uses. Such satellites are designed to operate in-orbit and have lifetimes of 10 years or more. Reliability, availability and maintainability (RAM) analysis of these systems has been indispensable in the design phase of satellites in order to achieve minimum failures or to increase mean time between failures (MTBF) and thus to plan maintainability strategies, optimise reliability and maximise availability. In this paper, we present formal modelling of a single satellite and logical specification of its reliability, availability and maintainability properties. The probabilistic model checker PRISM has been used to perform automated quantitative analyses of these properties.

Keywords

Markov processes; formal verification; probability; satellite communication; telecommunication computing; telecommunication network reliability; GLONAS; GPS; MTBF; RAM analysis; automated quantitative analysis; continuous time Markov chains; logical specification; mean time between failures; probabilistic model checker PRISM approach; reliability, availability and maintainability analysis; single satellite system; space based systems; Availability; Global Positioning System; Interrupters; Model checking; Probabilistic logic; Satellites; availability and maintainability (RAM) analysis; continuous time Markov chains (CTMCs); probabilistic model checking; reliability; satellite systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Modelling Symposium (EMS), 2013 European

Conference_Location

Manchester

Print_ISBN

978-1-4799-2577-3

Type

conf

DOI

10.1109/EMS.2013.102

Filename

6779914