Zachary Oster

This work is supported in part by US National Science Foundation grants CCF 1143734 and CCF 0702758.


Zachary J. Oster, Ganesh Ram Santhanam, and Samik Basu
Formal Methods & Verification Group, Department of Computer Science
Iowa State University


In goal-oriented requirements engineering, a goal model graphically represents relationships between the required goals (functional requirements), tasks (realizations of goals), and optional goals (non-functional properties) involved in designing a system. It may, however, be impossible to find a design that fulfills all required goals and all optional goals. In such cases, it is useful to find designs that provide the required functionality while satisfying the most preferred set of optional goals under the goal model’s constraints. We present an approach that considers expressive qualitative preferences over optional goals, as these can model interacting and/or mutually exclusive subgoals. Our framework employs a model checking-based method for reasoning with qualitative preferences to identify the most preferred alternative(s). We evaluate our approach using existing goal models from the literature.


Encoding CI-nets as Kripke structures for NuSMV

The NuSMV code used to encode the running example (the bookseller goal model) as a Kripke structure is contained in the following file:
cinet-ase11.smv (plain text, approx. 4K)

Goal models used in our paper

Each of these goal models has been modified from the original version cited in the paper and on this page. The Bookseller and Online Shop models have been modified only slightly, while the Trentino Transport model has been modified to a greater extent. Our intent was to be as faithful as possible to the original semantics of each goal model while adapting the models to better demonstrate the effectiveness of our framework.

Goal model 1: Bookseller (adapted from Liaskos et al., RE 2010)
Included in paper as running example (Figure 1)

Download a higher-quality PDF of this goal model (approx. 12K)

Goal model adapted from Sebastiani et al., RE 2010
Goal model 2: Trentino Transport (adapted from Sebastiani et al., CAiSE 2004)

Download a higher-quality PDF of this goal model (approx. 15K)

Goal model adapted from Sebastiani et al., CAiSE 2004
Goal model 3: Online Shop (adapted from Liaskos et al., CAiSE 2011 (to appear))
We thank Sotirios Liaskos for providing us with this goal model.