A Rigorous Approach to Requirements Validation

Visual notations such as the UML are popularly used by practitioners to model different aspects of a software system. In earlier work, we presented a semantics of UML object diagrams to facilitate visual modeling of requirements for business systems. In this paper, we present a comprehensive method for defining and validating the requirements of a system, based on formal analysis, automatic scenario generation, and support for rapid prototyping. Model-checking is used in the formal analysis to identify internal inconsistencies in the specification, and to generate interesting ´scenarios´ from the specifications that can help in identifying potentially incomplete or anomalous requirements. Prototype tools have been built for the automatable steps of the method, and it has been experimentally used to model and validate the requirements of two systems. The experiments resulted in identification of many inconsistencies and anomalies in the requirements of each of these systems