hould be defined, built and run; all errors They provide an invaluable insight into the user's view of how should be logged and at intervals a new build should be provided the system should be used. and the tests which identified bugs in the previous version should be 3. They provide a mechanism for agreement that the software is rerun. to specification and correct. Software design techniques 25/5 The tests are usually performed after the software has been in- In general they provide a way of applying a set of techniques as stalled, although the system test team may also run them during well as the technique itself: they are explained further below. system tests. In addition, there are specific techniques which may be used in conjunction with any software methodology; the main ones are 25.2.9 Maintenance and enhancements modelling, simulation and prototyping, and are explained in Section 25.5. These phases are often ignored, but in many ways may be deemed the most important as without them the software will have limited 25.3.1 Formal methods use and an even more limited lifetime. This is a set of methods based on the mathematical definition of the problem and solution. The main Formal Methods are VDM and Z, 25.2.9.1 Maintenance with HOL being favoured for protocol specification work. For VDM and Z there are limited tools available to support the creation All systems are prone to faults and however much testing has been of the specification and some syntax checking. For a few languages performed during development, it is extremely difficult, and often (for example B), some advances are being made in the provision of not cost effective, to continue testing until one is virtually certain proof related tools to allow formal verification of each subsequent that all faults are removed. Equally, hardware can, and will, fail stage of the design, proving correctness and completeness of each requiring some level of intervention. There are techniques available stage with respect to the previous stage. See also (Wing, 1990).