Formal development of robot software

The use of the formal method VDM in the development of a piece of control software for a simple robotics problem is described. The problem concerns the transfer of blocks from a conveyor belt to a pallet. An abstract specification of the problem is constructed and then refined to a more implementation oriented specification. The latter is translated in a semimechanical fashion to an implementation. The focus is on the nature of the two levels of specification. In the first it is ensured that the models used to represent the robot, pallet and conveyor belt interact correctly, ignoring implementation details such as how the robot moves. In the second the initial specification is refined to incorporate details of the robot's movement including the constraints on its movement which prevent it colliding with the pallet or the conveyor belt.