Description of the project

Rather often, software is written to deliver many features under time constraints. As a result, most of the time, a specification (describing what a program is aiming to do) is incomplete, out of date or (rather often) non-existent. In principle, a formal specification is rather useful, since it can be analysed for potential problems (such as deadlocks) and be used for test generation using a number of powerful techniques. This project aims to bring some of the benefits of formal specification, into the real world, by constructing abstract specifications (models) from code and hints from a developer. Here the aim is not to build a complete specification, but to capture the relevant part of a program behaviour which a developer considers important to analyse or to test from. In other words, a developer may only be interested in sophisticated testing of a particular part of a program (such as the one featuring complex state-transition behaviour); the project will deliver a tool to take Java/C++ code and relatively automatically (with some help from a developer) build a model and generate tests from it.

An abstract specification is expected to be represented in a form of an X-machine (extended finite-state machine). The project aims to build such specifications from code, reflecting the parts of it a developer is interested in, and subsequent test generation from these models. Model generation does not have to be perfect: the code is likely to contain defects, a number of which may become obvious once a model is shown to a developer. Regression testing, to check that changes to code did not break something which worked previously, is made easier by using such generated models. Indeed, since models are based on code, if a formal method applied to a model determines that a particular test is necessary, the relation to the code can be used to determine the corresponding test data. This solves a known problem with application of formal methods to real software.

Implementation of the techniques developed in the project is available from sourceforge.

Email me for more information (replace _ in the email address with @)