Research Home
Current Research
Past Research
Seminar Series


Current Research

The following sections provide further details and contacts for a number of our current research projects and interests:

Safety Analysis and Failure Modelling

Failure timing and sequencing issues in qualitative and quantitative safety analysis (ISAAC project) - Extending traditional analysis methods (e.g. FTA) for automatic safety analysis of designs of complex systems that include timing and sequencing relationships between basic and intermediate events. This includes: intuitive graphical representation of causal relationships and of temporal relationships between the events, extension of the concepts of cut-sets and minimal cut-sets for temporal context, methods for automatic generation of such analysis artefacts using model checker approach, quantitative analysis that takes into account timing and sequencing relationships between events (For details contact Oleg Lisagor, David Pumfrey, John McDermid)

Safety of reconfigurable systems - Safety of reconfigurable systems such as Integrated Modular Systems; Health monitoring for initiating reconfiguration on failure and processes for developing civil aerospace systems. (For details contact Mark Nicholson)

Systems of Systems Analysis and Justification

Hazard Analysis for Systems of Systems - Development of techniques for hazard analysis of complex systems of systems, using multi-agent simulation and logic programming. (For details contact Rob Alexander, Tim Kelly)

Safety Policy for Systems of Systems - Development of techniques to systematically derive and express a policy for ensuring the safety of agents operating as part of a system of systems. (For details contact Martin Hall-May, Tim Kelly)

Formal Software Development

Practical Formal Specification - Extending model-based design tools to the construction and formal analysis of abstract specifications of embedded control system software. (For details contact Ian Toyn, Andy Galloway, John McDermid, Frantz Iwu)

Proof vs Testing - Justifying the substitution of testing with proof in certification arguments based on "at least as convincing" and "no more expensive than". (For details contact: Andy Galloway, Richard Paige, Rob Weaver, John McDermid, Ian Toyn)

Reasoning about control law diagrams - Formalisation of control law diagrams using a combination of Z and CSP, and development of a verification technique for Ada implementations based on refinement. (For details contact Ana Cavalcanti)

Development of object-oriented concurrent programs - The design of Circus is our solution to combining data and behavioural specifications: Z and CSP. We are also exploring this issue in the context of object-oriented languages, with a particular focus on refinement, tools, and industrial applications. (For details contact Ana Cavalcanti)

Proof of Absence of Run-Time Error with Floating Point Arithmetic - Proof of absence of run-time errors when using real arithmetic in SPARK Ada. Defining a process for generating relevant verification conditions (VCs), and prototyping a tool which can post-process the output from the SPARK toolset and discharge the additional VCs. (For details contact Diyaa-Addein Atiya, Steve King, John McDermid)

Model Checking Circus - Integration of formal verification techniques of refinement model checking and theorem proving for Circus, a concurrent language for refinement that combines Z, CSP and Dijkstra's guarded commands. (For details contact Leonardo Freitas, Jim Woodcock, Ana Cavalcanti)

A Refinement Calculus for Circus - The objective of this work is to formalise a Refinement Calculus for Circus. As an extension of the existing refinement strategy for Circus, we also present a translation strategy for Circus programs, which can be used in the translation of Circus programs to Java. (For details contact Marcel Oliveira, Ana Cavalcanti, Jim Woodcock)

Real Time Systems

Analysis and development of real-time systems - Extension of Circus (a combination of Z and CSP) to include constructs of Timed CSP, which allow specification, and analysis of real time systems. We are concerned with the semantic model of the new language, and with the reuse of existing tools for CSP and Circus to reason about timed specifications. (For details contact Ana Cavalcanti, Jim Woodcock)

Systems and Software Architectures

Architecture-Based Development for Safety-Critical Software Applications - Architecture Design for Safety, Failure Modelling of Architectures, Architecture Evaluation and Refinement for Safety. (For details contact Weihang Wu, Tim Kelly)

Architectural Modelling for Managing Change in High Integrity Real Time Systems - Model Based Systems Engineering, Software Architectures, Modelling of Software Intensive Systems, Architectural Views and View Consistency in Models, Architecture Recovery, Design Erosion, Change Management in Software Lifecycle, Architectural Description Languages, Trusted Components. (For details contact Alek Radjenovic, Richard Paige)

Optimisation of Flexibility In Systems Architectures - Automated design trade-off using evolutionary algorithms, hill climbing algorithms and scenarios. Modelling and analysis of real-time systems architectures. (For details contact Paul Emberson, Iain Bate)

Safety Case Development

Safety Justification of Commercial off-the Shelf (COTS) Components - Certification Strategies for COTS components - including COTS Component Criticality analysis, Assurance Contracts, Mitigation Strategies and a Safety Case Pattern Language for COTS justfication. (For details contact Fan Ye, Tim Kelly)