Premium
Use of executable formal specifications in user validation
Author(s) -
Bülent Özcan Mehmet
Publication year - 1998
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(1998110)28:13<1359::aid-spe206>3.0.co;2-2
Subject(s) - executable , computer science , formal specification , specification language , language of temporal ordering specification , software engineering , programming language , formal methods , implementation , modular design , system requirements specification , programming language specification , software requirements specification , user requirements document , user interface , software development , software , software design , programming paradigm , inductive programming , programming domain
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. © 1998 John Wiley & Sons, Ltd.