Deriving operational software specifications from system goals

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.