Dr Helen Treharne

Research Interests

I’ve recently come back from attending the Intelligent Transportation Systems track at  ISOLA 2012 which was a very rewarding experience  providing the focus to identify common interests.  In November, we have a paper at  HVC 2012, my colleague Markus Roggenbach from Swansea will be presenting it. Meanwhile, I’ll be attending the RRUK conference in London to meet new people working in railway research. Also in November, David Williams will be visiting me from VU University, Amsterdam – we share an interest in many things including verification and fairness in model checking and on a completely different topic, delegation of authorization in Federated Identity Management Systems. In December Steve Schneider and I will be visiting Heike Wehrheim to continue our work on providing Event-B with a CSP failures semantics. So it is an exciting time leading up to the end of the year.

I am motivated to use formal modelling in various application domains. I have been involved in Formal Modelling for over 15 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. Islam is now working for TRL and James will be working for AWE. 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. He spent the first three months of his PhD at the company familiarising himself with the technology and now he has just successfully completed his first year.

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, Dr Markus Roggenbach and Prof Faron Moller.

Publications

Papers

Google Citations

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 2013 I will be teaching: 

• Software Engineering (COM1028). We have guest lectures on the course from Fidessa and Accenture.
• Data Structures and Algorithms (COM1029) with Professor Schneider.

In 2011-12 I taught three undergraduate modules

• Programming Fundamentals using Java (COM1027)
• Software Engineering (COM1028). We have guest lectures on the course from Fidessa and Accenture.
• Modelling and Simulation using CSP and JCSP (COM2007)

All modules are supported using a VLE with an emphasis on practical work. The Java Programming module is examined using a practical exam using Eclipse and a secure upload.

Departmental Duties

I am on sabbatical until February 2013. My main administrative duties for 2012-13 are the following:

• 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. During 2011-12 I was responsible for UCAS Co-ordination and Open Days, and a member of the Department Policy and Strategy Group.

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.