A project is being set up to write a back end processor for the property market. The back end will provide a number of generic functions for recording the details of clients, recording the details of properties, searching for properties according to various criteria, recording offers made, recording sales completed, and producing various managements reports. The back end is intended to support a number of different front ends, each of which will be used by a different firm of estate agents, and will provide the agent's own brand image. The deliverables from the project are a conceptual model of the view of property sales management supported by the back end, a specification of the back end in VDM, a Java implementation of the back end, a test harness for exercising the back end functions, and instructions for installing the system, for operating the test harness, and for writing applications to use the back end.
The development team have not got much VDM expertise, but a consultant is available to give advice, and to review the VDM specification after the first few weeks of the project.