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 @)