Unifying Theories of Programming and Testing
- 11:30 13th May 2009 ( week 3, Trinity Term 2009 )Room 478, Oxford University Computing Laboratory
In this talk we present our recent results on integrating theories of testing into Hoare and He's Unifying Theories of Programming (UTP). We show how the notion of conformance in testing relates to notions of refinement in programming. As an example, we discuss "ioco", Tretmans' commonly used input-output conformance relation over reactive processes, and present it in the style of UTP's predicative semantics. The underlying assumptions of this conformance relation are formulated as additional healthiness conditions over the alphabet of traces and refusal sets. This enables formal proofs of ioco-properties, e.g. its relation to CSP's process refinements. After the theory discussion we will give some insights into applications for automated test case generation: We show how automated ioco-checking has been applied in protocol testing and discuss how the theory points to a new test-case generator that is based on SMT solving.