Research Interests

Since first studying Communicating Sequential Processes (CSP) and the B-Method during my undergraduate studies at Surrey University I have had a keen interest in formal methods; in particular their applicability to industrial projects. Since starting my PhD in 2009, under the supervision of Dr. Helen Treharne and Prof. Steve Schneider, I have looked at using model checking in CSP for a variety of different applications. My PhD is partially funded by AWE plc. and this has lead to the current focus of the PhD.

I began my PhD by looking at applying mathematical rigour to semi-formal UML models, but the PhD focus has since evolved, and is now focused on formally verifying VHDL hardware descriptions. My current work explores the adaption of Bill Roscoe's SVA compiler to generate optimised CSP models of VHDL descriptions for analysis in the model checking tool FDR.  One of the key issues we face when model checking is state space explosion. Therefore, the style of CSP models used to represent a hardware description is critical to enabling the analysis of large complex VHDL descriptions.

The use of formal methods is a specialist, and primarily academic, area and is one of the key reasons that formal analysis is not often fully applied in the design methodology of safety critical systems. As a result, my work also focuses on applying formal verification of VHDL descriptions 'under the hood', thus making them more accessible within an industrial application. My approach is being implemented using meta modelling tools to automatically generate CSP models from VHDL descriptions and we aim to provide feedback in a suitable form for the VHDL designer based on the results of the formal analysis.

Publications

• James Sharp, Helen Treharne and Steve Schneider: Assessing the Applicability of SVA in Analysing VHDL Models 
• Islam Abdelhalim, James Sharp, Steve A. Schneider, Helen Treharne: Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP