Multi-Object Reasoning with Constrained Goal Models
  Goal models have been widely used in Computer Science to represent software
requirements, business objectives, and design qualities. Existing goal
modelling techniques, however, have shown limitations of expressiveness and/or
tractability in coping with complex real-world problems. In this work, we
exploit advances in automated reasoning technologies, notably Satisfiability
and Optimization Modulo Theories (SMT/OMT), and we propose and formalize: (i)
an extended modelling language for goals, namely the Constrained Goal Model
(CGM), which makes explicit the notion of goal refinement and of domain
assumption, allows for expressing preferences between goals and refinements,
and allows for associating numerical attributes to goals and refinements for
defining constraints and optimization goals over multiple objective functions,
refinements and their numerical attributes; (ii) a novel set of automated
reasoning functionalities over CGMs, allowing for automatically generating
suitable refinements of input CGMs, under user-specified assumptions and
constraints, that also maximize preferences and optimize given objective
functions. We have implemented these modelling and reasoning functionalities in
a tool, named CGM-Tool, using the OMT solver OptiMathSAT as automated reasoning
backend. Moreover, we have conducted an experimental evaluation on large CGMs
to support the claim that our proposal scales well for goal models with
thousands of elements.
