Formal Testing of Correspondence Carrying Software

Nowadays formal software development is characterised by use of multitude formal specification languages. Test case generation from formal specifications depends in general on a specific language, and, moreover, there are competing methods for each language. There is a need for a generic approach to formal testing and for sound ways of combining test case generation methods. We address these issues using Correspondence Carrying Software, a paradigm for integrating heterogeneous specifications using viewpoints and category theory. We illustrate our approach with a small example of a train system specified using OCL and Z