Microprocessors chips are in most devices we interact with in our daily lives. From mobile devices, TVs, cars, fridges, petrol station pumps, servers that power the web and social media infrastructure --- the list is endless. Microprocessors have been doubling in power roughly every two years following Moore's law, which has been enabled by making the features of the chips smaller, fitting more transistors per unit area and driving the entire consumer electronics market worth more than £1 trillion per year. In order to continue to satisfy the industrial and societal demand that drives Moore's law, there are some fluid dynamics modelling challenges that we need to overcome. The next-generation of photolithography machines that need to manufacture smaller, faster microprocessor chips and the new devices required to supercool the high-performance chips during operation can be enabled by understanding and predicting accurately how gases behave at the micro/nanoscales, or in vacuum-like conditions. In these multiscale flow problems, the fluid dynamics is often unintuitive and all equations we normally turn to for modelling and designing engineering flow problems, such as flow around aircraft and ships using Navier-Stokes equations, are no longer valid here, because the gas is no longer in local thermodynamic equilibrium, on which these classical equations are formulated. The direct simulation Monte Carlo (DSMC), is the state-of-the-art software for modelling these non-equilibrium gas flows. It is a stochastic particle method with large numerical stability and can resolve the molecular nature of gases in three dimensional geometries. However, because it is a particle method, it requires a voracious computational cost to produce engineering solutions of scales that matter to industry. DSMC also performs poorly if those flows are at low speed, due to the inherent thermal noise in the particles blocking the measurable signals. In this project, we propose developing a new multiscale method, one which combines DSMC with computationally cheaper models such as those used in Computational Fluid Dynamics (CFD). We will produce a step change in simulation efficiency and accuracy by connecting DSMC and CFD solvers using surrogate modelling and Bayesian inference. With strong backing from our industrial partners, we will turn the outcome of this project into a free open-source computational solver released in the UK's OpenFOAM software that is validated with experimental data. The industrial focus of this project will be on processor-chip manufacturing, chip thermal management and electrospray technologies, but the underlying method is general to new directions in other research and industrial areas.

Today's products from many manufacturing industries, notably aerospace, automotive and high-tech manufacturing, depend on embedded software to function. Since many of these products support safety or mission-critical services, the correctness of the embedded software is a paramount concern. Most of today's industrial efforts focus on improving the code review, testing and qualification process to achieve this. Whilst these processes can reveal defects, they cannot prove their absence. Further, finding defects at review, test or even integration time is too late. Significant engineering efforts have already occurred, making further changes complicated, costly, and uncertain. In contrast to testing approaches, formal verification can prove the correctness of software, substantially reducing the need for testing, whilst also increasing reliability. Formal verification has been investigated for three decades, but has matured significantly over the last few years. The proposers believe it is now possible to develop a verification framework that can verify Model-Driven Engineering (MDE) notations such as UML and SysML, which are widely used to develop embedded software. The proposers have previously mapped MDE descriptions in a custom notation into both source code and the process algebra CSP, allowing formal verification using FDR, a model checker also produced by the proposers. This led to verified embedded systems that contained 1M lines of code. This work was limited in the modelling languages, the system architectures, and execution semantics it supported and had no formal proof guaranteeing the source code generated was equivalent to the models being verified. It was also a point solution that could not interoperate with other tools, nor handle legacy code. The overall goal of this proposal is to produce an industrially-applicable framework that supports verification and implementation of MDE languages. We will also develop a proof-of-concept tool that supports our framework and allows both academic and industrial exploitation. At the core of our framework will be a new formal verification language, called Communicating Components (CoCo), that is designed to model embedded software written in MDE languages. FDR will be used to verify models expressed in CoCo; the recent step-change performance improvements in FDR3 mean we will be able to handle more complex components and architectures. We will also provide a translation from CoCo into source code. We will improve the reliability of the source code translator by using the Coq theorem prover to prove the translation preserves the semantics of the model. In addition to the MDE engineers who will benefit from this project, formal methods researchers will also benefit. We will develop new specification-directed abstraction and verification techniques, based on the compositional methods we used in our earlier verification work. Secondly, we will add extra functionality to FDR3 to support this work, and thereby make our work readily accessible to the large FDR3 community. We have assembled an enthusiastic group of industrial partners comprising Aerospace Technology Institute (leader of UK strategy for aerospace), ASML (world's largest supplier of photolithography systems), ASTC (global industry leader for tools and solutions in safety critical and real time control electronics industries), MBDA (world leader in missiles and missile systems) and Rolls-Royce CDS (leading provider of high integrity control systems), who will collaborate with us and provide essential industrial expertise across these industries. This will allow us to ensure that the framework and proof-of-concept tool we produce are industrially applicable. Our partners will also provide case studies and, we hope, ultimately provide users for our technology.