Bernhard Aichernig, Graz University of Technology, Austria/UNU-IIST, Macau
This course presents a testing theory that integrates into Hoare and He's Unifying Theory of Programming (UTP). We will demonstrate its application to mutation testing on various levels of abstraction: specification- and program-based test case generation.
We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. The result is a simple framework for reasoning over faults and test cases in a precise manner. After explaining the theoretical background, we will derive techniques for generating test cases that prevent certain faults from being implemented.
The theory is general and can be mapped to various styles of modelling. We show results of test cases generation from design-by-contract specifications and protocol models, the latter including a recent industrial application.