Current active interests and area of expertise
Using the model-checker SPIN to do test-generation for the open-source RTEMS operating system, in collaboration with the European Space Agency, and companies that help develop and maintain RTEMS.
Exploring UTP semantics for shared-variable concurrency as a baseline for exploring formal aspects of concurrent software development methodologies, in collaboration with Jim Woodcock.
Unifying Theories of Clocked Parallel Systems; Priority and Probability in same; Formal Semantics of Handel-C; UTP Theorem Prover development.
Past areas of interest: A new emerging area of interest and expertise is the application of formal modelling techniques to descriptions of complex software development processes, with a particular focus on the requirements of medical device software certification. Also of interest is being involved in advocating a more product-oriented approach to critical medical software certification, rather than the process focus that is currently employed. This work will be done in collaboration with colleagues from Lero.
Exploring the feasibility of formally proving the correctness of a Time-Space Partitioning Kernel (TSPK) , as part of the European Space Agency's Savoir-IMA activity.
Process Algbras with Unbounded Dual Non-determinism; External Effects of Functional I/O; Function-based Formal Methods. Silicon Compilation via Functional Languages;
FORMAL SEMANTICS OF HANDEL-C
Recent work has explored giving a formal semantics to Handel-C, by first considering a carefully chosen subset, designed to ensure all awkward language features are considered, to ensure full industrial applicability of the research results. This work has been done in collaboration with Professor Jim Woodcock of the university of York.
THEORIES OF CLOCKED PARALLEL SYSTEMS
I developed an expertise in the relatively new Unifying Theories Framework, with a view to using this framework to present my theories of hardware compilation in general, and Handel-C semantics in particular. Of particular interest in this area is an emerging theory of synchronous Circus, and a denotational semantics for Handel-C based on "hardware compilation". Also in collaboration with Professor Jim Woodcock.
EXTERNAL EFFECTS OF FUNCTIONAL I/O
A particularly strong move has been towards the formal modelling of input/output and real-world interactions in pure functional languages with referentially transparent I/O systems based either on monads, or uniqueness typing.
PROCESS ALGEBRAS WITH UNBOUNDED DUAL NON-DETERMINISM
In collaboration with Prof Joseph Morris at DCU, I am also working on a theory of process algebras with unbounded demonic and angelic non-determinism, developed by formally "lifting" a deterministic theory to the non-determinsistic level.
SILICON COMPILATION VIA FUNCTIONAL LANGUAGES:
My Ph.D. research (1990) explored the use of pure functional languages as a tool for supporting silicon compilation.
FUNCTIONAL-BASED FORMAL METHODS:
My main research interest then switched to formal modelling techniques with a pure functional flavour, as exemplified by work done as part of the "Irish School of VDM".
THE FACS PROJECT: I supervised a graduate student under the FACS project, looking into modifying the pi-calculus to describe the kinds of object-oriented systems developed using the CORBA object technology .
RESEARCH-LED CONSULTANCY In the period from July 1991, through to 1997/98, I was involved, through company "K&M Technologies", in research-led consultancy, looking to apply formal techniques in industry. Most clients were involved in telecommunications (Motorola, Ericsson). Some of this work was carried out through EU-funded RACE and ACTS projects (SCORE, Mobilise).