Dr Helen Treharne
Senior Lecturer
Qualifications: PhD, MSc, BSc, MBCS, FHEA
Email: h.treharne@surrey.ac.uk
Phone: Work: 01483 68 3161
Room no: 13 BB 02
Office hours
Tuesday 12:00-14:00. Drop me an email and I'm happy to arrange an appointment, or drop in if my door is open.Further information
Research Interests
I am looking forward to co-chairing the IFM conference with Diego in Pisa in June 2012 and I look forward to meeting you all there.
I am motivated to use formal modelling in various application domains. I have been involved in Formal Modelling for over 10 years with a particular interest in its application to the defence industry and more recently security related applications. In our Formal Methods and Security group we have developed two formal modelling approaches: CSP||B and Event-B||CSP.
We have being using formal modelling to underpin software and hardware languages so that informal models can benefit from rigorous analysis. Our CSP||B approach has been used to underpin executable UML. More recently, we have been applying the process algebra CSP to underpin fUML and also VHDL. Our current PhD students, Islam Abdel Halim and James Sharp are responsible for these contributions. The watermarking application domain has also provided an area which is amenable to verification. CSP has been used to successfully analyse buyer seller watermarking protocols and we have successfully found numerous attacks in existing protocols; David Williams, now a Research Fellow at Vrije Universiteit, Amsderdam, was responsible for this contribution.
More recently, a CASE KTN with Thales Research and Technology (UK) Ltd, is supporting us to investigate the potential of using formal modelling in the area of Federated Identity Management; Evangelos Aktoudianakis is the PhD student on this project and has recently spend a three month placement at the company familiarising himself with the technology.
My other interest is in text watermarking. Achieving a reasonable capacity whilst not compromising robustness is a major challenge. Chris Culnane, now a Research Fellow, in the Department, developed an excellent approach which was robust to printing and scanning as part of his PhD in this area.
Our Formal Methods and Security group has an active PhD group and some of the students receive sponsorship from Thales Research and Technology (UK) Ltd. and AWE plc..We also enjoy collaborating with Professor Heike Werheim and Dr Markus Roggenbach.
Publications
Papers
2012
Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, CSP||B modelling for railway verification: the Double Junction case study, Department of Computing Technical Report CS-12-03, 2012.
Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Combining event-based and state-based modelling for railway verification, Department of Computing Technical Report CS-12-02, 2012.
2011
- Steve Schneider, Helen Treharne & Heike Wehrheim, “Bounded Retransmission in Event-B||CSP: a Case Study”, B2011 Workshop, Limerick, 2011. PDF.
- Steve Schneider, Helen Treharne & Heike Wehrheim, “A CSP account of Event-B refinement”, REFINE'11: Refinement Workshop, Limerick, 2011. PDF.
- Steve Schneider, Helen Treharne & Heike Wehrheim, “Bounded retransmission in Event-B||CSP: a Case Study”. Department of Computing Technical Report CS-11-04, University of Surrey 2011. PDF
- Steve Schneider, Helen Treharne & Heike Wehrheim, “Stepwise Refinement in Event-B||CSP. Part 1: Safety”. Department of Computing Technical Report CS-11-03, University of Surrey 2011. PDF
- Islam Abdelhalim, Steve Schneider & Helen Treharne, “Towards a practical approach to check UML/fUML models consistency using CSP”, ICFEM 2011, 6991 LNCS:33-48 2011. PDF
2010
- Steve Schneider & Helen Treharne, “Changing system interfaces consistently: a new refinement strategy for CSP||B”. Science of Computer Programming, 2010. Volume 76, Issue 10, Pages 837–860 PDF
- Islam Abdelhalim, James Sharp, Steve Schneider & Helen Treharne, Formal Verification of Tokeneer Behaviours Modelled in fUML using CSP. ICFEM 2010. LNCS, Volume 6447/2010, 371-387. PDF
- Steve Schneider, Helen Treharne & Heike Wehrheim, A CSP Approach to Control in Event-B. IFM 2010. LNCS Volume 6396/2010, 260-274. PDF
- Jiang, W., Ho, A.T.S., Treharne, H., Shi, Y.Q., "A Novel Multi-size Block Benford's Law Scheme for Printer Identification”, PCM 2010 Springer LNCS Vol. 6297, p643-652, 2010 PDF
- Williams, D.M., Treharne, H., Ho, A.T.S., "On the Importance of One-Time Key Pairs in Buyer-Seller Watermarking Protocols," International Conference on Security and Cryptography, Secrypt 2010, 26-28 July 2010, Athens, Greece. PDF
2009
- Williams, D.M, Treharne, H., Ho, A.T.S., Waller, A., "Formal Analysis of Two Buyer-Seller Watermarking Protocols," Digital Watermarking (IWDW08), Springer, LNCS 5450, pp278-292, 2009. PDF
- Jiang, W., Ho, A.T.S., Treharne, H., "A Novel Least Distortion Linear Gain Model for Halftone Image Watermarking Incorporating Perceptual Quality Metrics," Transactions on Data Hiding and Multimedia Security IV, Springer-Verlag LNCS 5510, pp. 65-83, 2009. PDF
- Beeta Vajar, Steve Schneider & Helen Treharne, Mobile CSP||B. AVOCS 2009. Volume 23 EASST. PDF
- Steve Schneider & Helen Treharne, Changing system interfaces consistently: a new refinement strategy for CSP||B. IFM 2009, LNCS Volume 5423/2009, 103-117, PDF
2008
- Williams, D.M, Treharne, H., Ho, A.T.S., Culnane, C., "Using a Formal Analysis Technique to Identify an Unbinding Attack on a Buyer-Seller Watermarking Protocol," 10th ACM Workshop on Multimedia and Security, September 22-23, 2008, Oxford, UK. PDF
- Steve Schneider, Helen Treharne, Alistair McEwan & Wilson Ifill, Experiments in translating CSP || B to Handel-C. CPA 2008. PDF
- Edward Turner, Helen Treharne, Steve Schneider & Neil Evans, Automatic generation of CSP || B skeletons from xUML models. ICTAC 2008 Volume 5160/2008, 364-379. PDF
Teaching
In 2011-12 I teach three undergraduate modules
- Programming Fundamentals (COM1027)
- Software Engineering (COM1028). We have guest lectures on the course from Fidessa and Accenture.
- Modelling and Simulation (COM2007)
All modules are supported using ULearn with an emphasis on practical work. The Java Programming module is examined using a practical exam using Eclipse and a secure upload.
Departmental Duties
My main administrative duties for 2011-12 are the following:
- UCAS Co-ordinator
- Open Day Co-ordinator
- Member of Department Policy and Strategy Group
- Member of University Senate
- Member of University Quality and Standards Subcommittee with responsiblity for chairing validation panels.
From 2008-2011 I was the Undergraduate Director of Studies responsible for restructuring the undergraduate Computing programmes.
External duties
MSc External Examiner, Department of Computer Science, Aberystwyth University, Wales.
MSc External Examiner with responsibility for MSc in Business Information Technology and Software Engineering Management, Southampton Solent University.
Reviewer on EPSRC SafeCap project with collaborators at Newcastle and Swansea Universities.

