I've been involved in the following projects:
- Taming Concurrency, Newcastle University, 2013 to Present
Visit our group's Concurrency Reasoning webpage or see the
For this project, we are investigating the core issues in concurrency, using techniques such as abstraction and rely-guarantee reasoning.
The Newcastle and UQ concurrency groups held a joint meeting at Singapore in May 2014 and I visited UQ in December 2014.
Visit my Newcastle staff page.
Read the relevant papers here.
- A Model-Based Safety Analysis of Air Traffic Control Operational Procedures, UQ, 2011-2012.
This project used Behavior Trees and model checking to automate Failure Modes and Effects Analysis, to conduct a safety analysis
of an air-traffic control system.
For more information, visit the project page.
- Slicing Behavior Trees for Verification of Large Systems, PhD project, Griffith University, 2007-2011.
My PhD thesis is on using slicing techniques for reducing Behavior Tree specifications prior to model checking.
The thesis also includes the definition of a novel form of branching bisimulation which preserves the Next operator of CTL*,
while still allowing some stuttering steps to be removed.
Read the relevant papers or download my thesis here.
- Building Dependability into Complex, Computer-Based Systems, ARC Centre for Complex Systems, 2004-2008.
This project developed the Behavior Tree specification language.
I was involved in the automation of Failure Modes and Effects Analysis using Behavior Trees and model checking.
a translator from Behavior Trees to the input language of the SAL model checker, in the following versions: part of the TextBE drawing tool (C++ STL),
as a stand-alone tool (Visual C++ MFC) (both versions available here),
as part of the Integrare drawing tool (Visual C++ MFC), available here under "Tools" and
as part of the BTE drawing tool (Java) (no longer available).
I also developed the BTFail tool for modelling the effects of failures on Behavior Trees
and the CompTest tool for testing Java or .NET component implementations according to their BT specifications (both no longer available).
I developed another translator from Behavior Trees to the input language of the UPPAAL model checker, available as part of the Integrare tool above.
More details can be found on the ACCS page and in the following Annual Reports:
Annual Report 2004, page 17.
Annual Report 2005, page 19.
Annual Report 2006, page 21.
Annual Report 2007, page 24.
Annual Report 2008.
Read the relevant papers here.
- Cellular Automata as a Model for Dynamic Leaf Structure, BE Honours project, UQ, 2003.
For this project, I created a cellular automata model for leaf growth, which predicts area expansion rate when provided with linear expansion rates.
Read my honours thesis here.
- Minerosion 3.01, a user friendly erosion monitoring and landscape design package, School of Land and Food Sciences, UQ, Summer 2002-2003.
For this project I developed the GUI for the Minerosion 3.01 software package in Visual Basic.NET. This software appears to be no longer available.