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.

Investigating disease persistence in host vector systems: dengue as a case study

The investigation of pathogen persistence in vector-borne diseases is important in different ecological and epidemiological contexts. In this thesis, I have developed deterministic and stochastic models to help investigating the pathogen persistence in host-vector systems by using efficient modelling paradigms. A general introduction with aims and objectives of the studies conducted in the thesis are provided in Chapter 1. The mathematical treatment of models used in the thesis is provided in Chapter 2 where the models are found locally asymptotically stable. The models used in the rest of the thesis are based on either the same or similar mathematical structure studied in this chapter. After that, there are three different experiments that are conducted in this thesis to study the pathogen persistence. In Chapter 3, I characterize pathogen persistence in terms of the Critical Community Size (CCS) and find its relationship with the model parameters. In this study, the stochastic versions of two epidemiologically different host-vector models are used for estimating CCS. I note that the model parameters and their algebraic combination, in addition to the seroprevalence level of the host population, can be used to quantify CCS. The study undertaken in Chapter 4 is used to estimate pathogen persistence using both deterministic and stochastic versions of a model with seasonal birth rate of the vectors. Through stochastic simulations we investigate the pattern of epidemics after the introduction of an infectious individual at different times of the year. The results show that the disease dynamics are altered by the seasonal variation. The higher levels of pre-existing seroprevalence reduces the probability of invasion of dengue. In Chapter 5, I considered two alternate ways to represent the dynamics of a host-vector model. Both of the approximate models are investigated for the parameter regions where the approximation fails to hold. Moreover, three metrics are used to compare them with the Full model. In addition to the computational benefits, these approximations are used to investigate to what degree the inclusion of the vector population in the dynamics of the system is important. Finally, in Chapter 6, I present the summary of studies undertaken and possible extensions for the future work.

A critical study of John Hick's religious pluralism

This study examines the pluralistic hypothesis advanced by the late Professor John Hick viz. that all religious faiths provide equally salvific pathways to God, irrespective of their theological and doctrinal differences. The central focus of the study is a critical examination of (a) the epistemology of religious experience as advanced by Professor Hick, (b) the ontological status of the being he understands to be God, and further asks (c) to what extent can the pluralistic view of religious experience be harmonised with the experience with which the Christian life is understood to begin viz. regeneration. Tracing the theological journey of Professor Hick from fundamentalist Christian to religious pluralist, the study notes the reasons given for Hick’s gradual disengagement from the Christian faith. In addition to his belief that the pre-scientific worldview of the Bible was obsolete and passé, Hick took the view that modern biblical scholarship could not accommodate traditionally held Christian beliefs. He conceded that the Incarnation, if true, would be decisive evidence for the uniqueness of Christianity, but rejected the same on the grounds of logical incoherence. This study affirms the view that the doctrine of the Incarnation occupies a place of crucial importance within world religion, but rejects the claim of incoherence. Professor Hick believed that God’s Spirit was at work in all religions, producing a common religious experience, or spiritual awakening to God. The soteriological dimension of this spiritual awakening, he suggests, finds expression as the worshipper turns away from self-centredness to the giving of themselves to God and others. At the level of epistemology he further argued that religious experience itself provided the rational basis for belief in God. The study supports the assertion by Professor Hick that religious experience itself ought to be trusted as a source of knowledge and this on the principle of credulity, which states that a person’s claim to perceive or experience something is prima facie justified, unless there are compelling reasons to the contrary. Hick’s argument has been extensively developed and defended by philosophers such as Alvin Plantinga and William Alston. This confirms the importance of Hick’s contribution to the philosophy of religion, and further establishes his reputation within the field as an original thinker. It is recognised in this thesis, however, that in affirming only the rationality of belief, but not the obligation to believe, Professor Hick’s epistemology is not fully consistent with a Christian theology of revelation. Christian theology views the created order as pre-interpreted and unambiguous in its testimony to God’s existence. To disbelieve in God’s existence is to violate one’s epistemic duty by suppressing the truth. Professor Hick’s critical realist principle, which he regards as the key to understanding what is happening in the different forms of religious experience, is examined within this thesis. According to the critical realist principle, there are realities external to us, yet we are never aware of them as they are in themselves, but only as they appear to us within our particular cognitive machinery and conceptual resources. All awareness of God is interpreted through the lens of pre-existing, culturally relative religious forms, which in turn explains the differing theologies within the world of religion. The critical realist principle views God as unknowable, in the sense that his inner nature is beyond the reach of human conceptual categories and linguistic systems. Professor Hick thus endorses and develops the view of God as ineffable, but employs the term transcategorial when speaking of God’s ineffability. The study takes the view that the notion of transcategoriality as developed by Professor Hick appears to deny any ontological status to God, effectively arguing him out of existence. Furthermore, in attributing the notion of transcategoriality to God, Professor Hick would appear to render incoherent his own fundamental assertion that we can know nothing of God that is either true or false. The claim that the experience of regeneration with which the Christian life begins can be classed as a mere species of the genus common throughout all faiths, is rejected within this thesis. Instead it is argued that Christian regeneration is a distinctive experience that cannot be reduced to a salvific experience, defined merely as an awareness of, or awakening to, God, followed by a turning away from self to others. Professor Hick argued against any notion that the Christian community was the social grouping through which God’s Spirit was working in an exclusively redemptive manner. He supported his view by drawing attention to (a) the presence, at times, of comparable or higher levels of morality in world religion, when contrasted with that evidenced by the followers of Christ, and (b) the presence, at times, of demonstrably lower levels of morality in the followers of Christ, when contrasted with the lives of other religious devotees. These observations are fully supported, but the conclusion reached is rejected, on the grounds that according to Christian theology the saving work of God’s Spirit is evidenced in a life that is changing from what it was before. Christian theology does not suggest or demand that such lives at every stage be demonstrably superior, when contrasted with other virtuous or morally upright members of society. The study concludes by paying tribute to the contribution Professor Hick has made to the field of the epistemology of religious experience.