Themes investigated by the Testing Research Group include model-based testing, search-based testing, property-based testing, security verification and testing, model-driven engineering, reverse engineering, XML data processing, massively parallel multi-agent simulation and software engineering.
Our work on model-based testing using Stream X-Machines is internationally known. This formal testing method generates complete functional test suites from a model specification expressed as an extended finite state machine; and offers guarantees of correctness once testing is complete. The work has been used at Daimler for testing automotive systems designed using Harel Statecharts, applied to testing the gate-logic on low-power ARM chips, used for unit testing Java and also used to test software services for SAP and SingularLogic in the Cloud. Several software testing tools have grown out of this work, including StateTest, JWalk and Broker@Cloud.
Leaders: Dr Simons, Dr Bogdanov, Prof Holcombe
Our work on search-based testing is internationally known. This evolutionary testing method creates genomes for tests, which evolve by mutation and inter-breeding until superior tests are expressed, which are capable of exercising parts of software systems that are difficult to reach. Fitness is judged by instrumenting the tested code to measure what is covered by the tests. The approach has been applied to large C programs and also to object-oriented programs in Java. Several software tools have grown out of this work, including EvoSuite (for Java) and IGUANA (for C) and Code Defenders, the first crowd-sourced interactive mutation testing game.
Leaders: Dr McMinn, Dr Fraser
Property-based testing provides a high-level approach to testing and is a complementary technique to the similar model-based testing. Rather than focusing on individual test cases to encapsulate the behaviour of a system, in property-based testing this behaviour is specified by properties, expressed in a logical form. The system is then tested by checking whether it has the required properties for randomly generated data, which may be inputs to functions, sequences of API calls, or other representations of test cases. This work has resulted in a code coverage tool (Smother) and a mutation testing tool (Mu2) for the Erlang language.
Leaders: Prof Derrick, Dr Bogdanov, Dr Taylor
Security Verification and Testing
Security encompasses information security, software engineering, security engineering, and formal methods. Our research in this area investigates all security aspects of distributed and service-oriented systems. This includes applied security aspects, such as access control or business-process modelling, as well as fundamental aspects, such as novel static and dynamic approaches for ensuring the security of applications. We participate in the development of interactive theorem proving environments for Z (HOL-Z) and UML/OCL (HOL-OCL, which is integrated into a formal MDE tool-chain) and a model-based test-case generator (HOL-TestGen).
Leaders: Dr Brucker
In the future, software systems will not be created by writing program code, but rather generated from high-level abstract models that are closer to end-user requirements. What initial models and languages should be chosen? How should models be checked? How should they be folded together to create more detailed system specifications? How should the transformation rules be verified? Our work so far has investigated dependently-typed languages as a means of verifying model transformations, has generated simple information systems from requirements and has also generated platform-specific test suites for SOAP or REST-based software services in the Cloud.
Leaders: Dr Simons, Dr Brucker, Prof Derrick
This novel approach recovers specifications from legacy software systems. The reverse engineering method collects traces of the system's execution and performs grammar inference on the traces, to detect behavioural regularity. From this, finite state models are constructed, which allow further hypotheses about the specification to be generated and tested. The approach has been applied to recover both flat and nested state specifications, and used for the supervised re-modularisation of software systems. Software tools include StateChum (for reverse engineering) and SUMO (for supervised re-modularisation).
Leaders: Dr Bogdanov, Dr Hall, Dr Taylor
XML Data Processing
The rise of distributed data processing in the Cloud has led to a resurgence of non-relational key-value and tree-structured data formats like XML. This has opened up new research areas in XML data compression, distribution and storage, with associated issues of data indexing and query-processing. We have developed algorithms for fast searching in distributed XML databases using sparse binary matrix indexing; and for trust-based access control to XML data with dynamic learning. The technology has been applied in Botswana for the distributed mobile phone hosting of compressed XML databases.
Leaders: Dr North
Massively Parallel Multi-Agent Simulation
This radical approach to simulation is able to model the interacting behaviour of massive populations of individual agents on Grid or HPC parallel architectures. The detail offered by individual-based modelling is fast outpacing traditional aggregating methods that use calculus. We have modelled the behaviour of social insect colonies, the transfer of proteins, the growth of epithelial skin cells, and even the performance of the European economy! We have discovered new facts about ants, or the best way to recover from the financial crisis. The FLAME (Flexible Large-scale Agent-based Modelling Environment) tool developed by the VT-Group is now also used by our Computational Biology and Graphics Research groups, among others.
Leaders: Dr Richmond, Dr McMinn
Why do software development projects frequently fail, and what can be done about it? This strand of our research has investigated both traditional and agile software development methods, to see how they work in practice. We have published internationally-famous critiques of the UML notation and associated development process, and also of the Agile method known as XP (eXtreme Programming). We have collaborated with work psychologists to monitor the behaviour and effectiveness of developer teams in our own software company Genesys Solutions, revealing how the constitution of teams affects how well they work.
Leaders: Dr Cowling, Dr Simons