  Navigation satellites are a core component of navigation satellite based
systems such as GPS, GLONASS 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 10 years or more. Reliability,
availability and maintainability (RAM) 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 (MTBF) 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.
