Formal development methods for interactive systems: Combining interactors and design rationale

This thesis builds upon existing research on the formal aspects of human-computer interaction by providing practical specification and development methods for interactive systems. The specification style used is based on the abstract concept of interactors, which has been used extensively at York. The development methods are integrated with a way in which design options that occur may be recorded and choices between them made so that a more constructive development process is provided between the programmer and the client. This thesis has two strands. In the first strand, a notation DQN (Design Question Notation) is defined in order to provide a general link between design rationale research and formal methods. For simplicity, examples are expressed using Morgan's refinement calculus. In the second strand, specification and development methods are defined for interactors, based on extensions that are made to CSP and Action Systems. As well as the standard refinement relations for inter..