Probabilistic verification of satellite systems for mission critical applications

In this thesis, we present a quantitative approach using probabilistic verification techniques for the analysis of reliability, availability, maintainability, and safety (RAMS) properties of satellite systems. The subject of our research is satellites used in mission critical industrial applications. A strong case for using probabilistic model checking to support RAMS analysis of satellite systems is made by our verification results. This study is intended to build a foundation to help reliability engineers with a basic background in model checking to apply probabilistic model checking to small satellite systems. We make two major contributions. One of these is the approach of RAMS analysis to satellite systems. In the past, RAMS analysis has been extensively applied to the field of electrical and electronics engineering. It allows system designers and reliability engineers to predict the likelihood of failures from the indication of historical or current operational data. There is a high potential for the application of RAMS analysis in the field of space science and engineering. However, there is a lack of standardisation and suitable procedures for the correct study of RAMS characteristics for satellite systems. This thesis considers the promising application of RAMS analysis to the case of satellite design, use, and maintenance, focusing on its system segments. Data collection and verification procedures are discussed, and a number of considerations are also presented on how to predict the probability of failure. Our second contribution is leveraging the power of probabilistic model checking to analyse satellite systems. We present techniques for analysing satellite systems that differ from the more common quantitative approaches based on traditional simulation and testing. These techniques have not been applied in this context before. We present the use of probabilistic techniques via a suite of detailed examples, together with their analysis. Our presentation is done in an incremental manner: in terms of complexity of application domains and system models, and a detailed PRISM model of each scenario. We also provide results from practical work together with a discussion about future improvements.

A practical MEMS gravimeter

The ability to measure tiny variations in the local gravitational acceleration allows – amongst other applications – the detection of hidden hydrocarbon reserves, magma build-up before volcanic eruptions, and subterranean tunnels. Several technologies are available that achieve the sensitivities required (tens of μGal/√Hz), and stabilities required (periods of days to weeks) for such applications: free-fall gravimeters, spring-based gravimeters, superconducting gravimeters, and atom interferometers. All of these devices can observe the Earth tides; the elastic deformation of the Earth’s crust as a result of tidal forces. This is a universally predictable gravitational signal that requires both high sensitivity and high stability over timescales of several days to measure. All present gravimeters, however, have limitations of excessive cost (£70 k) and high mass (<8 kg). In this thesis, the building of a microelectromechanical system (MEMS) gravimeter with a sensitivity of 40 μGal/√Hz in a package size of only a few cubic centimetres is discussed. MEMS accelerometers – found in most smart phones – can be mass-produced remarkably cheaply, but most are not sensitive enough, and none have been stable enough to be called a ‘gravimeter’. The remarkable stability and sensitivity of the device is demonstrated with a measurement of the Earth tides. Such a measurement has never been undertaken with a MEMS device, and proves the long term stability of the instrument compared to any other MEMS device, making it the first MEMS accelerometer that can be classed as a gravimeter. This heralds a transformative step in MEMS accelerometer technology. Due to their small size and low cost, MEMS gravimeters could create a new paradigm in gravity mapping: exploration surveys could be carried out with drones instead of low-flying aircraft; they could be used for distributed land surveys in exploration settings, for the monitoring of volcanoes; or built into multi-pixel density contrast imaging arrays.