Professor Helen Treharne
Academic and research departments
School of Computer Science and Electronic Engineering, Department of Computer Science, Digital World Research Centre.About
Biography
Helen is a Professor in the Department of Computer Science. 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 she has been awarded follow on funding to continue development and collaboration with Watts Gallery, Compton, the Lightbox, Woking and Visit Surrey. Some of the project team is featured in a YouTube video describing the project.
University roles and responsibilities
- Member of Faculty Executive Board
- Head of School of Computer Science and Electronic Engineering
Previous roles
Responsibilities outside of the University
Current roles
- Director (Education) of Surrey Academic Centre of Excellence in Cyber Education (ACE-CSE, Surrey received gold award from NCSC)
- Asscociate Editor ACM Computing Surveys
Previous roles
- MSc External Examiner with responsibility for Business Information Technology and Software Engineering Management MSc, Southampton Solent University.
- Surrey University membership of the Rail Research UK Association (RRUKA).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.
ResearchResearch 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 Computer Science, 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 Computer Science 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.
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 Computer Science, 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 Computer Science 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.
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.
Publications
Papers
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 Computer Science 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 Computer Science 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 Computer Science 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 Computer Science 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