Seminars & Workshops

The Twilight Zone: from testing to formal specifications and back again

Speaker:	Koen Claessen , Chalmers University of Technology, Gothenburg, Sweden
When:	2009-12-15 09:00
Place:	Room B103, Bldg 39, SNU

Abstract

This talk aims to shine some light on the grey area that lies in between two related but different topics: testing and formal specifications. Testing is the most widely used verification method used by software developers of all walks of life; formal specifications are an unambiguous means of stating what software should do and not do.

The red thread going through the talk is the popular property-based testing tool QuickCheck. QuickCheck uses random testing to check formal specifications that are written in a restricted executable logic, producing minimal counter examples to failing properties. Thus, using QuickCheck we generalize the act of executing a specific test case against a specific expected behavior, to the act of executing many automatically generated test cases against a general specification.

This is a very powerful method, but it also introduces a number of issues. Firstly, where does the general specification come from? Often, just formally specifying software seems equally hard as implementing it! Secondly, how should a general specification be expressed as a testable property? Thirdly, what test data should we generate?

The talk contains ongoing work in different efforts within our research group to deal with these issues: We are developing a companion tool to QuickCheck that uses random testing to automatically generate specifications from programs -- a good starting point for a full formal specification of the program. We are looking at how we can systematize the path that starts from a high-level logical specification and that ends with an effective list of testable properties -- this path often consists of non-trivial choices. We also have a way of calculating which particular kinds of test data polymorphic functions should be tested on.

Finally, the talk addresses some of the open questions that we do not have good answers to. In particular, we will see examples of software that is extremely hard to test effectively using methods that are known to us.