A survey on the formalisation of system requirements and their validation

System requirements define conditions and capabilities to be met by a system under design. They are a partial definition in natural language, with inevitable ambiguities. Formalisation concerns with the transformation of requirements into a specification with unique interpretation, for resolving ambiguities, underspecified references and for assessing whether requirements are consistent, correct (i.e. valid for an acceptable solution) and attainable. Formalisation and validation of system requirements provides early evidence of adequate specification, for reducing the validation tests and high-cost corrective measures in the later system development phases. This article has the following contributions. First, we characterise the specification problem based on an ontology for some domain. Thus, requirements represent a particular system among many possible ones, and their specification takes the form of mapping their concepts to a semantic model of the system. Second, we analyse the state-of-the-art of pattern-based specification languages, which are used to avoid ambiguity. We then discuss the semantic analyses (missing requirements, inconsistencies etc.) supported in such a framework. Third, we survey related research on the derivation of formal properties from requirements, i.e. verifiable specifications that constrain the system’s structure and behaviour. Possible flaws in requirements may render the derived properties unsatisfiable or not realizable. Finally, this article discusses the important challenges for the current requirements analysis tools, towards being adopted in industrial-scale projects.