Deriving manuals from formal specifications. Extended version

In this paper we propose the use (or re-use) of formal specifications for the development of user manuals and user instructions. We base our work on two observations. The first is that a considerable part of user manuals consist of series of user instructions that guide a user in the use of a device or a software application. The second is that the user interface in terms of user operations and feedback can often be described in the form of a finite state machine. In this paper we describe how model checking techniques can be used to derive automatically series of user instructions from the interface specification. The approach is illustrated by means of the specification of a well-known device such as a telephone which is then used to derive proper instruction sequences addressing relevant 'how-to' and 'what-if' questions about the operation of the system from a user point of view.