Use of Synchronous Concurrent Algorithms in Development of Safety Related Software

University of Swansea 1994-2004 (part-time)

Imagine a way to reduce the costs and introduction of errors whilst developing High integrity software – the software that is in flight control/medical/nuclear/defence systems.

Mathematical models are used to describe requirements, design, and implementations of key critical aspects. These models are costly to write and prove correctness, and typically different models/languages are used in each phase, introducing additional costs to prove correctness across models.

My thesis introduced the use of Synchronous Concurrent Algorithms (SCAs) as a way of reducing the cost. Both algorithms and hardware can be separately described as SCAs, which can be defined algebraically.

My contribution was to extend the standard notation of SCAs and introducing a meta-algebra that supports the application of an algebraic process to translate an algorithm described as an SCA into hardware implementation described as another SCA (put very loosely: an algebraically correct method of compilation).