Model Checking Requirements

In software engineering, system requirements are written in a natural language such as English. Later in the design phase, these requirements are usually translated to a semi-formal language such as UML. This design model gives support to the development of the system in a programming language. Although natural language is easy to use, it is intrinsically ambiguous. Undesired effects may arise, as the errors generated by misinterpretation of the requirements can lead to a late discovery of a problem with a costly solution. In this paper, we propose the use of a Controlled Natural Language (CNL) (a subset of English that obeys a formal grammar) as a language for writing requirements. Moreover, we developed a translator from a CNL to the modelling language of the NuSMV model checker. In addition, we propose another CNL to describe properties in the style of a temporal logic. A second translator transforms this CNL into Computation Tree Logic. Therefore, our toolset allows the user to benefit from the user-friendliness of a natural language and to perform a formal analysis on the requirements using the NuSMV model checker. We are thus able to assert whether the requirements satisfy a property. The user only deals with CNLs as we hide all formal languages involved in the inputs of a model checker. Counter-examples are produced in the NuSMV notation, but they are fairly intuitive to understand. We illustrate our work in a case study.