| Abstract: | The use of the formal design method FOCUS is illustrated by an example development of the so-called Stenning-protocol. The development process starts from global, non-constructive service specifications and ends in executable programs of the protocol entities. The four abstraction levels of FOCUS - trace specification, functional specification, abstract program, and concrete program - are covered. Special emphasis is put on the design steps within and between the first two abstraction levels, which are also proven correct |
