Test Case Extraction from Correctness Proofs

Extract from the Case for Support:

 A large and diverse body of Computing Science research is devoted ultimately to the goal of finding ways to produce computer systems that are reliable and behave correctly.  Traditionally, the techniques of testing and formal proof have been viewed as competing means of achieving this end, perhaps complementing each other, but essentially separate.   The aim of this research is to develop and study a method which synergistically combines both of these techniques.

 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:

The full Case for Support is now available in postscript format.  This gives a more detailed description of the project including a diagrammatic workplan.

Savi Maharaj