Flaws in requirements may have severe impacts on the subsequent phases of the development flow. These also undermine the formal verification activity, which typically formalizes the requirements into formal properties that are considered as golden and used to check the correctness of the design or software/hardware implementation. Most of the efforts in formal methods have historically been devoted to comparing a design against a set of requirements. The validation of the requirements themselves, however, has often been disregarded and poses several challenges. First, requirements are often written in natural language, and may thus contain a high degree of ambiguity. Second, the informal requirements often express global constraints on the system-to-be (e.g., mutual exclusion), and, in order to retain a direct connection with the informal requirements, the formalization cannot follow standard model-based approaches, but must be complemented with more suitable formalisms such as temporal logics. Third, the formal validation of requirements suffers from the lack of a clear correctness criterion (which in the case of design verification is basically given by the availability of high-level properties). Finally, the expressiveness of the language used in the formalization may go beyond the typical level used for formal verification (e.g., propositional logic).
The methodology for requirements analysis proposed in the PROSYD project [FRV1, FRV2] is based on a series of checks in terms of satisfiability of LTL to verify the consistency of properties, their compatibility with some scenario, and their entailment of some assertions. This work has been extended to more expressive logic to represent requirements of hybrid systems [FRV3, FRV4] and to temporal satisfiability modulo theories [FRV5]. Other formal checks that can be used to pinpoint issues in the requirements specification are based on the notions of realizability [FRV6], vacuity [FRV7], or unconstrained outputs [FRV8].