Abstract

In traditional engineering disciplines – such as mechanical or structural engineering – product safety is often described in terms of “mean time between failures”. Absolute reliability is either not possible, or – even where it might be possible – is regarded as too expensive.

It might seem that software engineering is not subject to the same considerations: after all, software weighs nothing! However, over-designing the software component of a system, such as an aircraft avionics sub-system, can easily lead to over-designed hardware; and this will have an effect on the economic viability of the project. One simple and extremely pertinent example will suffice: how many decimal places need to be set aside for each real number to ensure that all arithmetic operations in a flight-control computer are correctly rounded?

Having a formalized continuous mathematics enables us to specify the correctness of computer control systems in terms of a model for the world in which they operate. One can describe the system of differential equations in which the system operates, and then prove that the required probability of the system behaving correctly is met. With luck, this process might be susceptible to extensive automation.

The talk will assume no specialized knowledge of Probability, Integration or Measure; nor will an extensive knowledge of PVS be assumed.