Use of executable formal specifications in user validation

Requirements validation through feedback with users is of paramount importance in producing a high quality requirements specification document. Use of an executable formal specification offers an effective combination of formalism and pragmatism. This allows not only the systematic development of a concise specification of a system, but it also enables developers to execute the specification to receive feedback at an early stage. Executable formal specification languages have traditionally been used as an effective prototyping tool to facilitate developer validation, that is the developer can, via specification execution either individually or in a peer review format, explore the consequences of the specification. However, their use in requirements validation is often not user orientated, which may in turn reduce the effectiveness of the approach. This paper reports on work to facilitate the user validation process based on executable formal specifications. A user orientated process with a systematic framework can maximise the effectiveness of the user validation process. Dialogue management based on scenarios enables an effective communication between a system and its users. Our approach also enables the intertwining of equational specifications in a modular algebraic specification language and conventional implementations in a modular programming language, This introduces a judicious choice of rigour, techniques and tools to support the user dialogue with a prototype system to effectively and explicitly address the user validation process. (C) 1998 John Wiley & Sons, Ltd.