The few approaches concerned with goal operationalization are the NFR framework

It is concerned with the elicitation of stake-holders goals, the elaboration of these goals into requirements on the software behavior, and the assignment of responsibilities for these requirements to agents . Inadequacy in the execution of any of these RE subtasks inevitably leads to development problems which are often difficult and costly to repair. This has led researchers to seek rigorous and automated methods to support the fulfillment of these tasks. Goal-oriented approaches have been shown to be particularly effective for formal analysis and automated validation. Goals are objectives the system is intended to achieve through the cooperation of agents in the envisioned software and its environment. “Reverse thrust enabled when a plane is moving on the runway” is an example of a goal for a Flight Control System (FCS). An operational requirement captures the conditions under which a system component may or must perform an operation to achieve the goals (e.g., a required precondition for disabling the reverse thrust is that the wheels’s pulse is on). One of the difficulties in developing a system specification is the elaboration of operational requirements that guarantee the satisfaction of the goals. This is essentially a manual task and hence is costly and error prone. Very little systematic, rigorous support exists; among the exceptions are the informal techniques explained in and the formal approaches in. A such approaches lack desirable characteristics such as automation and/or generality, making them less accessible to practitioners. the problem of how formal, tool supported methods can be effectively used to identify and resolve the incompleteness of a given set of operational requirements with respect to a set of predefined goals. We propose an integrated use of model checking to detect incompleteness in a given partial operational requirements specification, and inductive learning to resolve the incompleteness. The model checking formally verifies the satisfaction of the goals and produces a counterexample when an incompleteness is detected in the partial operational requirements specification.