AbstractZ is a formal notation for writing system specifications that has been growing in popularity over recent years. This paper examines some of the issues involved in applying a ‘partition based’ testing method to a system specified in Z. Details of an extensive case study are given, from specification and implementation of the system to the development and execution of test cases. The strategy is found to have benefits compared to those based on less formal specifications, but there are limitations to the approach, and difficulties that need address