Continuous Probability Distributions in Model-Based Specification Languages (2012)
The full text of this thesis is available from the Newcastle University Library website: https://theses.ncl.ac.uk/dspace/handle/10443/1696
Andrews, Z.H., School of Computing Science, University of Newcastle upon Tyne
Model-based specification languages provide a means for obtaining assurance of dependability of complex computer-based systems, but provide little support for modelling and analysing fault behaviour, which is inherently probabilistic in nature. In particular, the need for a detailed account of the role of continuous probability has been largely overlooked. This thesis addresses the role of continuous probability in model-based specification languages. A model-based specification language (sGCL) that supports continuous probability distributions is defined. The use of sGCL and how it interacts with engineering practices is also explored. In addition, a refinement ordering for continuous probability distributions is given, and the challenge of combining non-determinism and continuous probability is discussed in depth. The thesis is presented in three parts. The first uses two case studies to explore the use of probability in formal methods. The first case study, on flash memory, is used to present the capabilities of probabilistic formal methods and to determine the kinds of questions that require continuous probability distributions to answer. The second, on an emergency brake system, illustrates the strengths and weaknesses of existing languages and provides a basis for exploring a prototype language that includes continuous probability. The second part of the thesis gives the formal definition of sGCL's syntax and semantics. The semantics is made up of two parts, the proof theory (transformer semantics) and the underpinning mathematics (relational semantics). The additional language constructs and semantical features required to include non-determinism as well as continuous probability are also discussed. The most challenging aspect lies in proving the consistency of the semantics when non-determinism is also included. The third part uses a final case study, on an aeroplane pitch monitor, to demonstrate the use of sGCL. The new analysis techniques provided by sGCL, and how they fit in with engineering practices, are explored.