Congratulations to Wilson Ifill for successfully passing his PhD viva
Thursday 31 January 2008
Congratulations to Wilson Ifill for successfully passing his PhD viva on Friday 25th January. Willson’s thesis is titled: "B annotations in critical control systems development". The external examiner was Dr Mike Poppleton of the University of Southampton, and the internal was Dr Bill Mitchell. Willson was supervised by Professor Steve Schneider.
Abstract:
"The design and implementation of critical controllers benefit from development in a formal method such as B. However, B does not support execution specification directly. The aim here is to develop a set of annotations to be used by B design engineers to capture execution requirements, whilst creating the B state model. The annotations, once shown to be machine-annotation consistent with the B machine, can be used independently from the machine to assess the correctness, or guide the synthesis, of CSP controllers. The talk covers annotations proof obligations, annotation consistency conditions, refinement and translated into a hardware description language."