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.

Utility and safety of invasive (fractional flow reserve) and non-invasive (cardiac magnetic resonance imaging) diagnostic tests in patients with NSTEMI

A prospective randomised controlled clinical trial of treatment decisions informed by invasive functional testing of coronary artery disease severity compared with standard angiography-guided management was implemented in 350 patients with a recent non-ST elevation myocardial infarction (NSTEMI) admitted to 6 hospitals in the National Health Service. The main aims of this study were to examine the utility of both invasive fractional flow reserve (FFR) and non-invasive cardiac magnetic resonance imaging (MRI) amongst patients with a recent diagnosis of NSTEMI. In summary, the findings of this thesis are: (1) the use of FFR combined with intravenous adenosine was feasible and safe amongst patients with NSTEMI and has clinical utility; (2) there was discordance between the visual, angiographic estimation of lesion significance and FFR; (3). The use of FFR led to changes in treatment strategy and an increase in prescription of medical therapy in the short term compared with an angiographically guided strategy; (4) in the incidence of major adverse cardiac events (MACE) at 12 months follow up was similar in the two groups. Cardiac MRI was used in a subset of patients enrolled in two hospitals in the West of Scotland. T1 and T2 mapping methods were used to delineate territories of acute myocardial injury. T1 and T2 mapping were superior when compared with conventional T2-weighted dark blood imaging for estimation of the ischaemic area-at-risk (AAR) with less artifact in NSTEMI. There was poor correlation between the angiographic AAR and MRI methods of AAR estimation in patients with NSTEMI. FFR had a high accuracy at predicting inducible perfusion defects demonstrated on stress perfusion MRI. This thesis describes the largest randomized trial published to date specifically looking at the clinical utility of FFR in the NSTEMI population. We have provided evidence of the diagnostic and clinical utility of FFR in this group of patients and provide evidence to inform larger studies. This thesis also describes the largest ever MRI cohort, including with myocardial stress perfusion assessments, specifically looking at the NSTEMI population. We have demonstrated the diagnostic accuracy of FFR to predict reversible ischaemia as referenced to a non-invasive gold standard with MRI. This thesis has also shown the futility of using dark blood oedema imaging amongst all comer NSTEMI patients when compared to novel T1 and T2 mapping methods.