The formal development of robot software

A description is given of the use of the formal method VDM (C.B. Jones, 1986), in the development of a piece of control software for a simple robotics problem taken from W.E. Snyder (1985). The problem concerns the transfer of blocks from a conveyor belt to a pallet. An abstract specification of the problem is constructed which is then refined to a more implementation-oriented specification. The latter is then translated in a semi-mechanical fashion to an implementation. The authors concentrate on the nature of the two levels of specification. In the first, they ensure 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, they refine the initial specification 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