“Lean” formal methods in the development of provably correct real-time systems

Designing software to control real-time, reactive embedded applications is non-trivial. And as the complexity of such systems increases, the present industrial practice for their development gives cause for concern, especially, if they are to be used in safety-critical applications. In order for the design of these systems to be optimised, it is necessary to take into account the interdependence of the hardware and software. Thus, the system needs to be assessed at all stages of the development life-cycle in order to minimise the potential for errors. This has resulted in the development of a wide range of techniques which aim to support the analysis and design of both systems and their associated software. These vary from those with sound mathematical basis (formal methods) to structured methodologies. The latter while useful, do not provide a satisfactory and comprehensive solution. The former, on the other hand, are recognised as the most likely solution to the problem, but insufficient expertise and a lack of tool support have limited their practical deployment to highly specialised applications