Formal reasoning for analyzing goal models that evolve over time

In early-phase requirements engineering, modeling stakeholder goals and intentions helps stakeholders understand the problem context and evaluate tradeoffs, by exploring possible "what if" questions. Prior research allows modelers to make evaluation assignments to desired goals and generate possible selections for task and dependency alternatives, but this treats models as static snapshots, where the evaluation of the fulfillment of an intention remains constant once it has been determined. Using these techniques, stakeholders are unable to reason about possible evolutions, leaving questions about project viability unanswered when the fulfillment of goals or availability of components is not guaranteed in the future. In this article, we formalize the Evolving Intentions framework for specifying, modeling, and reasoning about goals that change over time. Using the Tropos language, we specify a set of functions that define how intentions and relationships evolve, and use path-based analysis for asking a variety of "what if" questions about such changes. We illustrate the framework using the Bike Lanes example and prove correctness of the analysis. Finally, we demonstrate scalability and effectiveness, enabling stakeholders to explore model evolution.