This paper presents a technique for automatically generating test-data to test exceptions. The approach is based on the application of a dynamic global optimization based search for the required test-data. The authors' work has focused on test-data generation for safety-critical systems. Such systems must be free from anomalous and uncontrolled behaviour. Typically, it is easier to prove the absence of any exceptions than proving that the exception handling is safe. A process for integrating automated testing with exception freeness proofs is presented as a way forward for tackling the special needs of safety critical systems. The results of a number of simple case-studies are presented and show the technique to be effective. The major result shows the application of the technique to a commercial aircraft engine controller system as part of a proof of exception freeness. This illustrates how automated testing can be effectively integrated into a formal safety-critical process to reduce costs and add value. Copyright © 2000 John Wiley & Sons, Ltd.

We discuss issues in the development of formal methods for use in aerospace applications, reflecting our experience in working with both Rolls-Royce and British Aerospace. We discuss some of the key factors which we believe govern the application of discrete mathematics to aerospace applications, drawing comparisons with applied engineering mathematics in other domains. We give an overview of three projects (the three "small steps"): the development of a domain-specific language for aircraft engine control system specification; the development of a formal semantics and tool support for state transition systems to facilitate analysis of specifications produced by systems engineers; the use of formalism in support of test automation. We then discuss the "gap" we see between the needs of industry and the current focus of the formal methods research community by pointing out important facets of industrial applicable formal methods which are not receiving adequate attention. We refer to this as a "giant leap" due to the need for a cultural shift in the research community and the need for a coherent approach to the identified research issues rather than piecemeal studies of the issues. Our conclusions are to be optimistic for the future use of formal methods in industry albeit with concern that their potential will not be realised unless there is a shift in emphasis within the research community?.

One of the major costs in a software project is the construction of test-data. This paper outlines a generalised test-case data generation framework based on optimisation techniques. The framework can incorporate a number of testing criteria, for both functional and non-functional properties. Application of the optimisation framework to testing specification failures and exception conditions is illustrated. The results of a number of small case studies are presented and show the efficiency and effectiveness of this dynamic optimisation-base approach to generating test-data.

Structural testing criteria are mandated in many software development standards and guidelines. The process of generating test data to achieve 100% coverage of a given structural coverage metric is labour-intensive and expensive. This paper presents an approach to automate the generation of such test data. The test-data generation is based on the application of a dynamic optimisation-based search for the required test data. The same approach can be generalised to solve other test-data generation problems. Three such applications are discussed-boundary value analysis, assertion/run-time exception testing, and component re-use testing. A prototype tool-set has been developed to facilitate the automatic generation of test data for these structural testing problems. The results of preliminary experiments using this technique and the prototype tool-set are presented and show the efficiency and effectiveness of this approach.