Dr Helen Treharne

Research Interests

I've recently returned from a Departmental sabbatical. Now I'm back in the swing of teaching Software Engineering and Data Structures and Algorithms and my research interests continue grow. 

• Our collaboration with Swansea and our colleagues Markus Roggenbach and Faron Moller is going well, we are developing abstraction and composition techniques to support the safety verification of railway interlocking systems. We presented papers at  the Intelligent Transportation Systems track at  ISOLA 2012 and at  HVC 2012. In May 2013 I will be attending the Nasa Formal Methods workshop in May 2013 where I have a short paper with one of my undergraduate students, Matthew Trumble and my Swansea collaborators. Matthew was funded on an EPSRC vacation bursary which was very successful and enjoyable. This is a great way to introduce bright students to research.
• Our work on defining policy templates for access control as a security mechanisms in social networks is growing. In collaboration with Evan Aktoudianakis, my PhD student, Thales Research and Technology (UK) Ltd., Jason Crampton  (RHUL) and Steve Schneider, we have defined an initial notation and now we are looking to extend the work to deal with cross network policy templates and policy evaluation.
• Our work with David Williams from VU University Amsterdam is looking at verification and fairness in model checking.
• Our work with Heike Wehrheim is further developing our ability to provide Event-B with a CSP semantics, this has led to new ways of dealing with liveness properties in Event-B.

So it is an exciting beginning to the year. I have also been very lucky to have been awarded a Royal Academy/Leverhulme Fellowship during 2013-2014 to continue to examine the model checking of railway interlocking systems.

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.

We currently hold 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 is now in his second year and getting to grips with novel contributions.

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 am 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

My main administrative duties for 2012-13 are the following:

• Member of University Senate
• Member of University Quality and Standards Subcommittee which involves chairing validation panels.
• Responsible for BCS validation in 2014.

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.

Member of the advisory board for the EPSRC SafeCap project with collaborators at Newcastle and Swansea Universities.

Member of the Rail Research UK Association (RRUKA).