The IMPRESS Project

`IMPRESS' was a project conducted at the School of Computing and Mathematics at University of Huddersfield. between 1996 and 1998, and was supported by the EPSRC, the MoD, and the National Air Traffic Services. It was aimed at developing and evaluating the application of machine learning techniques to the validation of requirements specifications written in customised, many-sorted first order logic. A precise requirements model can be viewed as an imperfect theory of the requirements domain that needs to undergo refinement to remove bugs or to reflect changes in the domain, and the problem can be formulated as one of theory revision. To drive the research we used an air traffic control requirements model (the `CPS') developed in a previous project called FAROAS. The model represents aircraft separation criteria and conflict prediction procedures relating to airspace over the North East Atlantic, and, inclusive of flight information, amounts to several thousand axioms.

The main results were as follows:

- the project succeeded in applying learning techniques to the validation of the CPS requirements model. This was accomplished using classified tests of the major function of the CPS (i.e. conflict prediction) as training examples. The CPS can be animated by a tool that translates it into a clausal form, and executes it using a Prolog interpreter. Training examples which are mis-classified by the CPS's animated form were investigated with the help of meta-interpreter technology. `Blame assignment' techniques were used to pin-point suspect clauses, and theory revision algorithms implemented to find revisions of the clauses. Two major obstacles during the research were (1) standard meta-interpreters could not cope with general clause form theories, in particular negation in clause bodies. We overcame this problem by designing a meta-interpreter to expand out negative literals. This could then build up proof trees from calls to negative as well as positive literals, and hence produce more accurate proof trees for analysis by the blame assignment phase. (2) efficiency of theory revision: we overcame the combinatorial problems inherent in theory revision using a bias that restricts revisions to `ordinal' literals and operators. In technical specifications such as the CPS, axioms involving comparisons and limits often make up the most complex conditions and hence are most prone to error.

- the design, implementation, and testing of integrated tools making up an automated validation environment for a large requirements model written in customised many-sorted logic has been accomplished. The environment incorporates two theory revision algorithms aimed at ordinal revision. One is based on hill climbing and implemented using simple ordinal revision operators. The second implements composite, focussed operators for inducing complex requirements. While the first algorithm has been used successfully to find and remove bugs in the CPS, the second has been used to update the CPS by inducing the formalisation of new requirements.

Personnel involved with the project included:

• Prof Lee McCluskey (principal investigator)
• Mrs Margaret West
• Dr Chris Bryant
• Dr Julie Porteous
• Dr Colin Pink
• Ms Carolyn Endeacott

For further details on IMPRESS email: impress@hud.ac.uk

IMPRESS and related FAROAS Publications