Compositional Testing
Channel: ETAPS 2017
Date: 09/05/2017

Invited tutorial, given by Kenneth McMillan (Microsoft Research Redmond, USA).

While full formal proof of complex systems remains a challenge, formal methods can readily be applied in practice to improve the performance of testing in exposing design errors. A good example of this is compositional testing. In this methodology, each component of a system is given a formal specification and it is proved formally that these specifications guarantee system-level correctness. The components are then rigorously tested against their formal specifications. This approach has the advantages of unit testing in covering component behaviors, while at the same time exposing all system-level errors to testing. Moreover, it can expose latent bugs in components that are not stimulated in the given system but may occur when the component is re-used in a different environment. This tutorial will cover the basics of compositional testing by example, introducing the available tools, and will also discuss industrial applications.