Research — Overview

The common theme of my research is formal analysis, which can be viewed as typically consisting of two aspects: modelling and verification. In a general sense, verification means demonstrating that a system satisfies certain requirements, and the term refers to a range of techniques. I am concerned with the application of methods that are formal in that they have a basis in mathematical logic and make use of formal models. Specifically, the verification techniques that I am applying in my work are deductive theorem proving and model checking.

An important part of any formal analysis activity is modelling and abstraction, as verification by theorem proving or model checking relies on the existence of a formal model. In fact, building an abstract model of a system already has benefits in itself: the chance of detecting, at an early stage of system development, subtle mistakes, inconsistencies and incompleteness.

I have been applying formal analysis methods to systems of various domains, such as programming languages, business processes, and wireless sensor networks. My particular interest is in safety-critical and fault-tolerant systems, for which the need for proper verification to substantiate claims of correctness and dependability is well understood in order to justify the trust placed in the correct and expected working of these systems. A significant part of my work in this domain has been carried out in the context of the Time-Triggered Architecture.