Dr Helen Treharne

Biography

Helen is the current interim Head of Department of Computing from March 2015 and a Senior Lecturer in the Department. Her established research interests lie in the areas of formal modelling of access control policies and railway verification. She has been awarded a Royal Academy of Engineering/Leverhulme Trust Senior Research Fellowship during 2013-2014 to continue to examine the model checking of railway interlocking systems.

Recently, she has been involved in an exciting multi-disciplinary project which is developing a mobile application and using augmented reality in museum spaces. Building on the success of the project we have now been awarded follow on funding to continue development and our collaboration with Watts Gallery, Compton, the Lightbox, Woking and Visit Surrey. Some of my project team feature in a YouTube video describing our project.

Research Interests

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. We have been applying the process algebra CSP to underpin fUML and also VHDL. More recently, we have been using CSP to provide a formal semantics for Event-B. Our recent PhD students in this area, Islam Abdel Halim and James Sharp are now working for TRL and AWE respectively.

Access Control and Federated Identity. Currently involved in a project with Thales UK Research & Technology which is examining ways to define scalable access control policies in a distributed federated identity management system.

Developing Applications for the Art Sector. This is a new exciting emerging interest, which combines my passion for the arts and the application of technology within it.

Previously, I have been involved in text watermarking. Achieving a reasonable capacity whilst not compromising robustness is a major challenge. Chris Culnane, now a Research Fellow, in our Department, developed an excellent approach which was robust to printing and scanning as part of his PhD in this area. The watermarking application domain has also provided an area which is amenable to verification and therefore provided an opportunity to tie both interests together. 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, Amsterdam, was responsible for this contribution.

Research Collaborations

The following detail Helen’s current research collaboration in the different research areas of interest.

Beyond The Visual (II): Augmented Realities in Spaces of Exhibition (IAA-funded, 1 year project) (start date: September 2013)

After the success of Beyond The Visual (I), Helen continues to collaborate with colleagues, Dr Chris Culnane from the Department of Computing, Dr Caroline Scarles from the Department of Tourism and Dr Matthew Casey from Pervasive Intelligence Ltd. The team have received funding to further develop the technology used in the first product. In this project, the team will develop a production-ready AR application which is capable of supporting the identified needs of curators. The requirements of the application are driven by our project partners, Visit Surrey, Watts Gallery and The Lightbox (all based in Surrey) and will be evaluated through two further live trials.  For further information please do contact Helen directly on: h.treharne@surrey.ac.uk. Project budget: £51,766K

Beyond The Visual: Augmented Realities in Spaces of Exhibition (EPSRC-funded, 1 year project) (start date: October 2012)

Helen is collaborating with colleagues Drs. Chris Culnane and Matthew Casey from the Department of Computing and Dr Caroline Scarles from the Department of Tourism at the University of Surrey as well as two local exhibition spaces (Watts Gallery and The Lightbox) to explore new ways in which technology through smartphones, tablets and augmented reality content can extend what is traditionally a primarily visual experience to one that is entirely multi-sensual. The research team are currently developing cutting-edge software that not only maps visitor movements inside such sites, but also provides visitors with additional augmented material through their handheld devices. For further information please do contact Helen directly on: H.Treharne@surrey.ac.uk. Project budget: £10K

Access Control Policy and identity assurance (CASE KTN-funded, 3.5 year project) (start date: July 2011)

Our work on defining policy templates for access control as a security mechanisms in social networks was recently being presented at Privacy Security and Trust 2013 in July. In collaboration with Evan Aktoudianakis, my PhD student, Thales Research and Technology (UK) Ltd., Prof. Jason Crampton  (RHUL) and Prof. 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.

Railway Modelling and Verification

Our collaboration with Swansea and our colleagues Dr Markus Roggenbach and Prof. 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,  HVC 2012. and at the NASA Formal Methods workshop in May 2013. At NFM we had a short 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 and we look forward to continuing in the Autumn. In the meantime, we're hoping to attend the FM-RAIL-BOK workshop in Madrid in September 2013.

Theoretical Foundations of Formal modelling and Verification.

Our work with Dr David Williams from VU University Amsterdam is looking at verification and fairness in model checking.

Our work with Prof. 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.

Publications

Papers

Google Citations

2012

• Steve Schneider, Helen Treharne, Heike Wehrheim, The behavioural semantics of Event-B Refinement,  Formal Aspects of Computing, October 2012. DOI 10.1007/s00165-012-0265-0
• Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Railway modelling in CSP||B: the double junction case study,  AVOCS 2012 (to appear).
• Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider & Helen Treharne, Defining and Model Checking Abstractions of Complex Railway Models using CSP||B, HVC 2012 (to appear).
• Islam Abdelhalim, Steve Schneider, Helen Treharne: An Optimization Approach for Effective Formalized fUML Model Checking. SEFM2012: 248-262
• Islam Abdelhalim, Steve Schneider, Helen Treharne: An integrated framework for checking the behaviour of fUML models using CSP, International Journal on Software Tools for Technology Transfer, 2012, DOI: 10.1007/s10009-012-0243-0
• 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 2014 I am teaching Java Fundamentals to the incoming Level 4 students.

In previous years I have taught

• Software Engineering (COM1028). We have guest lectures on the course from Fidessa and Accenture.
• Data Structures and Algorithms (COM1029) with Professor Schneider.
• 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

From March 2015 I am the interim Head of Department.

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

Current:

MSc External Examiner with responsibility for MSc in Business Information Technology and Software Engineering Management, Southampton Solent University.

Surrey University membership of the Rail Research UK Association (RRUKA).

Previous external responsibilities included:

MSc External Examiner, Department of Computer Science, Aberystwyth University, Wales.

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