Research

I work on the challenge of building dependable computer systems. Traditionally, such systems are built using formal techniques that rely on modelling and thorough analysis during design. However, modern network-based systems challenge the assumptions that underpin classical techniques. Modern systems are open, heterogeneous and flexible while traditional formal development techniques rely on highly specialised analysis techniques being applied to static models. My research addresses two questions: can we build systems that reconfigure in response to threats, yet remain verifiably trustworthy; and can we lower the entry barriers to using formal methods for building trustworthy systems?

Entry Barriers to Formal Methods

I’ve been actively involved in the Vienna Development Method (VDM). The focus in recent years has been on developing strong tools, resulting in a commercial toolset, VDMTools, and some significant industry applications. Advances in VDM itself mean that the method now deals with object-oriented, concurrent, distributed and real-time systems. A very active VDM network exists, including researchers at Newcastle, in Denmark, Japan, Portugal and the Netherlands. The Overture Initiative is the community-based development of a next generation of VDM Support Tools based on an open source framework and working within Eclipse.

My main technical interest in VDM is support for formal reasoning. This ranges from the underlying logic to the problem of providing effective support for user-guided proof. A particular interest is in the use of a logic that treats partial functions in a way that is more natural for computer systems development than the approach taken in classical logics.

 

Relevant current projects: Deploy

Predictable Dynamic Resilient Systems

Can we model and analyse dynamic systems so that we can predict their resilience to faults and threats in spite of their ability to change dynamically? We take an approach based on the use of formal modelling to help obtain predictability, and the use of run-time metadata to help identify and respond to failures and threats. In the context of Virtual Organisations, work has shown that we can develop exploratory environments that allow domain experts to experiment with policies for governing VOs. We’ve extended the approach to the development of access control models. In providing run-time resilience, work on the acquisition and use of run-time metadata to allow component-based systems to reconfigure in accordance with policies in response to threats. The use of Resilience-related Metadata is being taken forward in the new UK Software Systems Engineering Initiative (SSEI) in 2008-2011.

 

Relevant current projects: TrAmS, ReSIST and SSEI. 

Current PhD Students:

  • Kamarul Abdul-Basit, who is beginning a PhD on adaptive fault tolerance for self-organising systems.
  • Zoe Andrews, who is starting work on combining stochastic and logical reasoning in dealing with dependability arguments.
  • Anirban Bhattacharyya, who is working on formal models for reconfiguration in real-time systems.
  • Igor Mozolevsky, who is working on the formal analysis of access control policies that can be applied in dynamic coalitions.
  • Richard Payne, who examining formal descriptions of architectural reconfiguration.