The basic idea behind our approach is that, given a formal proof of the correctness of an abstract model of a system to be developed, we can extract data to be used in testing concrete implementations of that system. Our hypothesis is that this approach will remedy shortcomings inherent in both proof and testing: it will bolster the proof approach by plugging the gap between the abstract model whose correctness is proved and the actual implementation, and it will facilitate testing by providing test data which is especially effective at finding flaws.
Our objectives are: the development of techniques for test case extraction from proofs; an automated tool to support these techniques; an empirical evaluation of the techniques and tools by means of case studies; a theoretical and empirical characterization of the effectiveness of the techniques. The tools we develop will be general-purpose, capable of being put to use in a variety of application domains. However, we shall initially apply them to problems drawn from the areas of railway signalling systems, telecommunications and medical equipment software because the research group at Stirling have prior experience and links with organisations working within these domains.
We will structure our research into four main tasks: