Research Interests
  • Agent-based Modelling. The main contribution is the development and use of (Communicating) X-machines as a modelling language. This provides for a precise definition of both the individual and collective behaviour of agents by specifying their state transitions, internal memory and communication protocols. A very successful application of X-machine is the flexible large-scale agent modelling environment (FLAME) developed at the University of Sheffield. This is a template driven framework for agent-based modelling on parallel architectures ideally suited to the simulation of cellular and social systems. FLAME has been chosen by NERC (Natural Environment Research Council) in the UK as part of their Bio-Linux package. Another application of X-machine and FLAME is an innovative approach to macroeconomic modelling and economic policy design, proposed by EURACE, a FP6 EU project.

  • Model based Testing. Main contributions are the development of very powerful test generation methods from (deterministic, non-deterministic, communicating) stream X-machines that determine the correctness of the implementation under test, provided that the specification meets some, well defined, "design for test" requirements. Techniques for refining test sets in parallel with the specification have also been devised. As part of the EvoMT project, these methods have been complemented by evolutionary techniques to test generation from state-based formalisms. Since the translation of industrial standard languages such as UML statecharts into X-machines is immediate, all these methods have strong industrial application potential.

  • Modelling, Verification and Testing of Biology-inspired Computing Systems. One of the most promising computational to biosystem modelling is membrane computing (P systems). Membrane systems (also called P systems) are among the few computational models for biosystems that convincingly combine specification languages for quantitative, qualitative and topological system aspects with flexible mechanisms to capture the inherent parallelism of biochemical reactions. Although in the last years there have been significant developments in using the membrane system paradigm to model, simulate and formally verify various systems, testing, until recently, has been completely neglected. As part of the EvoMT project, we have developed an approach to testing various classes of P systems, based on a combination of coverage criteria, state based techniques and model checking. This is complemented by temporal logic and model checking based formal verification for implementations in NuSMV, Spin and ProB.

  • Evolutionary testing from Event-B and state-based models. The Event-B language is an evolution of the highly-successful B language, focused on software system modelling. The concerted efforts of the (academic and industrial) Event-B community to reiterate the success of B have been supported by two European research projects: RODIN, which produced a first platform for Event-B called Rodin, and DEPLOY, which is currently enhancing this platform based on industrial feedback. Motivated by industrial interest in model based testing, as part of the DEPLOY project, we have applied evolutionary techniques to test generation from Event-B models, proposing general forms for the corresponding fitness function. The approach has been implemented and its efficiency has been proven on a carefully designed benchmark using statistically sound evaluations.

  • Agile Modelling and Testing. Testing is a major part of software development and in XP (Extreme Programming) the generation of test cases is a vital part of the initial phases of a project. One of the key aspects of Extreme Programming is that unit tests have to be available before starting to write any code and have to be automated. X-machines can be integrated into Extreme Programming in a simple and designer-friendly way and have proven excellence in the construction of functional test sets.