Goal orientation is an increasingly recognized paradigm for eliciting,
modeling, specifying and analyzing software requirements.
Goals are statements of intent organized in AND/OR refinement
structures; they range from high-level, strategic concerns to lowlevel,
technical requirements on the software-to-be and assumptions
on its environment. The operationalization of system goals
into specifications of software services is a core aspect of the
requirements elaboration process for which little systematic and
constructive support is available. In particular, most formal methods
assume such operational specifications to be given and focus
on their a posteriori analysis.
The paper considers a formal, constructive approach in which
operational software specifications are built incrementally from
higher-level goal formulations in a way that guarantees their correctness
by construction. The operationalization process is based
on formal derivation rules that map goal specifications to specifications
of software operations; more specifically, these rules map
real-time temporal logic specifications to sets of pre-, post- and
trigger conditions. The rules define operationalization patterns that
may be used for guiding and documenting the operationalization
process while hiding all formal reasoning details; the patterns are
formally proved correct once and for all. The catalog of operationalization
patterns is structured according to a rich taxonomy of
goal specification patterns.
Our constructive approach to requirements elaboration requires a
multiparadigm specification language that supports incremental
reasoning about partial models. The paper also provides a formal
semantics for goal operationalization and discusses several semantic
features of our language that allow for such incremental reasoning.