Abstract :
A technique is presented for obtaining a specification from a requirement through a series of incremental steps. The starting point is a problem frame description involving a requirement on the phenomena of the problem domain, and a decomposition of the environment into domains, connected to one another and to the machine being implemented by shared phenomena. In each step, the requirement is moved towards the machine, leaving behind a trail of `breadcrumbs´ in the form of domain assumptions. Eventually, the transformed requirement references only phenomena at the interface of the machine and can therefore serve as a specification. Each step is justified by an implication that can be mechanically checked, ensuring that, if the machine obeys the derived specification and the domain assumptions are valid, the requirement will hold. The technique is applied to the logging subproblem of a radiotherapy system
