Nisansala Yatapanage

Dr. Nisansala Prasanthi Yatapanage
Research Associate
School of Computing Science
Centre for Software Reliability
Newcastle University, UK

I've been a researcher in formal methods since 2004. My research interests are in the verification of systems which exhibit a high degree of complexity, making them prone to errors and difficult to verify. I am particularly interested in safety-critical systems, which can potentially have serious impact. My research explores the various challenges associated with such systems, including methods to handle the concurrency aspects and methods for conducting failure analyses on systems that include potentially faulty hardware components.

Currently, I'm working at Newcastle University in the UK on the Taming Concurrency project. This project aims to investigate the fundamental aspects of concurrency, comparing the various methods for handling concurrency in order to extract an understanding of these core aspects. With Cliff Jones, I published a paper at SEFM 2015 (see below), which explores the use of abstraction for handling problems with strong separation of components, providing an alternative approach to the common separation logic methods. This abstraction solution helps to shed light on the fundamental qualities of separation. Similarly, we are now investigating a concurrent garbage-collection algorithm using rely-guarantee methods, in an attempt to understand the underlying qualities exhibited by such systems. Visit my staff page. Read the relevant papers here.

Previously, in my hometown Brisbane, I worked on several projects at Griffith University and The University of Queensland (UQ), as part of the ARC Centre for Complex Systems, on the verification of safety-critical systems using the Behavior Tree specification language, a language which maintains strong links between the natural language requirements and the formal model. My research focussed on using Behavior Trees and model checking to automate safety analyses. Read the relevant papers here.

My PhD thesis (obtained in 2012 from Griffith University, supervised by Kirsten Winter from UQ and Geoff Dromey at the start) is on the use of slicing techniques to reduce Behavior Tree models prior to model checking, to allow large systems to be verified. I also developed a novel form of branching bisimulation, called Next-preserving Branching Bisimulation, which allows stuttering behaviour to be removed while still preserving full CTL*, including the Next operator (see my journal paper listed below). Read the relevant papers or download my thesis here.

Following my PhD studies, I applied the failure analysis technique to an air-traffic control system for a project at UQ funded by NICTA.

Details of these projects can be found on my projects page.

See my papers or my thesis .

Latest News

Recent papers:
Reasoning about Separation using Abstraction and Reification with Cliff B. Jones published in SEFM 2015
Next-preserving Branching Bisimulation with Kirsten Winter published in Theoretical Computer Science.
For details of both and to watch the Audioslides presentation for the TCS paper, see my papers page.

Recent conferences/workshops I attended:
Kent Concurrency Workshop, Canterbury, 21st to 22nd July, 2016
Northern Concurrency Meeting, Newcastle, 2nd Dec, 2016
SEFM, York, 9th to 11th Sep, 2015
CONCUR, Madrid, 1st to 4th Sep, 2015
Imperial Concurrency Workshop, London, 15th to 16th July 2015