Verifying reactive systems by talking to them

In the system analysis phase of the classical software development cycle, requirements are defined; although this process can be systematic in some sense, requirements capture is usually intuitive and informal, and they are often expressed by natural language sentences. This process aims to obtain a general description of functional requirements (what the program should do) and non-functional requirements (as resources, performance etc.). Since requirements should be satisfied by the system, functional requirements must be checked with respect to the program. Temporal logics have been recognized as a useful means to express formally properties, and hence requirements, of reactive systems, and model checkers have been realized to check properties, written as temporal logic formulae, on the semantic model of a system. Our experience on this formalization has shown that many imprecisions frequently occur in the passage from informal expressions of system properties, expressed by natural language expressions, to temporal logic formulae. These imprecisions are mainly due to the inherent ambiguities derived from different interpretations of natural language expressions. We thus looked for an answer to this problem in Natural Language Understanding techniques [1,6], trying to develop a tool that would help to generate logic formulae, by working out ambiguities by means of interactions with the user.