Integrating Automated Testing with Exception Freeness Proofs for Safety Critical Systems

In the Proceedings of 4th Australian Workshop on Safety Critical Systems and Software. Australian Computer Society. November 1999.

Nigel Tracey, John Clark, Keith Mander and John McDermid.

The exception handling code of a system is in general the least documented, tested and understood part, since exceptions are expected to occur only rarely. This paper presents a technique for automatically generating test-data to test exceptions. The approach is based on the application of a dynamic global optimisation 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 it is to prove 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. An evaluation shows the application of the technique to a commercial aircraft engine controller system as part of a proof of exception freeness.

Back to Publications.