Search

The thesis goal is to explore the relations between Formal Verification techniques in Computer Science and Stochastic Analysis in Mathematics. They both deal with probabilistic dynamical systems, implying that the number of connections is significant. The Formal Verification studies dynamical systems' properties, which are specified in terms of logic statements. This discipline has been successfully applied to multiple industry problems, such as ``verification of'' Software, Microprocessors or Neural Networks. The models studied have a countable states space and this can be considered the main obstacle to extend Formal Verification techniques for the computation of likelihoods in the case of Stochastic Differential Equations. However, the most studied properties in Formal Verification have a clear characterization in Mathematics. In this thesis, we focus on the safety property ``always'', which can be characterized as an exit time in the theory of Stochastic Analysis. The main difficulties are twofold. Firstly, if we are particularly interested in discretizing the states space - going from a continuous, uncountable space to a finite countable one - it is very likely to have an explosion of the cardinality of the states space. This leads to problems both in time and memory complexity. We find a new characterization of the barycenter of a discrete probability measure, which allows us to introduce a new algorithm for the recombination problem. Then, we use the algorithm to build recombining trees in order to approximate weakly stochastic processes, solving the exponential explosion of the cardinality of the states space. Secondly, one has to consider the approximation error: if the probability to exit from a safety region has not an analytical closed-form, a numerical scheme must be considered and therefore it is important to analyse the error. We introduce a grid-free approach for the computation of Probabilistic Safety Regions using Malliavin Calculus.

We have explored applications of Augmented Reality (AR) for external beam radiotherapy to assist with treatment planning, patient education, and treatment delivery. We created an AR development framework for applications in radiotherapy (RADiotherapy Augmented Reality, RAD-AR) for AR ready consumer electronics such as tablet computers and head mounted devices (HMD). We implemented in RAD-AR three tools to assist radiotherapy practitioners with: treatment plans evaluation, patient pre-treatment information/education, and treatment delivery. We estimated accuracy and precision of the patient setup tool and the underlying self-tracking technology, and fidelity of AR content geometric representation, on the Apple iPad tablet computer and the Microsoft HoloLens HMD. Results showed that the technology could already be applied for detection of large treatment setup errors, and could become applicable to other aspects of treatment delivery subject to technological improvements that can be expected in the near future. We performed user feedback studies of the patient education and the plan evaluation tools. Results indicated an overall positive user evaluation of AR technology compared to conventional tools for the radiotherapy elements implemented. We conclude that AR will become a useful tool in radiotherapy bringing real benefits for both clinicians and patients, contributing to successful treatment outcomes.

A numerical model has been developed for the simulation of the vacuum heat treatment and high pressure gas quenching used during the manufacture of single crystal turbine blades, of the type used for aeroengine applications. Heat transfer by radiation and forced convection is taken into account to obtain quantitative predictions of the thermal history of the components during ramping-up, holding and gas fan quenching. The uniformity of the temperature is investigated and the effectiveness of the treatment is assessed. Simulations of the quenching process have allowed visualisation of the flow field and prediction of the local quench rate as a function of the furnace parameters. The results of the modelling have been validated against thermocouple measurements made on laboratory-scale vacuum furnace with many of the characteristics of the type used in industrial production. The modelling methodology is extended to industrial scale processes via a multi-scale decomposition approach. The effect of quench rate on the microstructure of CMSX-10 has been characterised using scanning electron microscopy. It is shown that the precipitate size distribution correlates directly with the local quenching rate. To understand the influence of the microstructure on creep performance, two structures with different average \(\gamma\)’ size have been tested in creep over a wide range of temperatures and applied stress levels. Particularly in the low temperature / high stress regime, the size of the precipitates markedly determines the creep performance observed.