The first work package addresses scaling the property-based testing approach. Even though systems of almost a million lines of code have been tested with property-based testing, so far this work has concentrated on testing certain components and a subset of the functionality of these systems and, in turn, this has resulted in a number of isolated models that each encapsulates some aspects of the system. We will develop a method to compose such models into a single system model. In testing large systems parts need to be mocked, and we will develop techniques that use the same property models to also take care of the mocking activity. Thirdly, we will design methods to reduce state space explosion in testing by modelling aspects of a system that are not relevant to the test in question.