Dr. Nabendu Chaki

Title: Model Checking using Goal Models 

Abstract: Goal Modelling techniques are typically used to identify and detect errors, conflicts, or issues that may arise in the later phases of the life cycle. Early detection of errors between project goals helps in reducing the cost to a great extent. In our efforts to assess the advantages of applying model checking on goal models, we have used i* framework and developed the i*ToNuSMV tool.
The i* is one of the most complex multi-agent modelling frameworks. We have used it for requirements engineering. Actors and inter-dependencies between the Actors are said to be intentional for the i* framework. The i*ToNuSMV tool acts as a POC for the proposed Semantic Implosion Algorithm where we can feed i* models and temporal specifications as input and check whether the specifications are satisfied by the model.
The NuSMV model checker runs in the back end to verify the specification and generates a counterexample if it fails to satisfy. The goal model reconciliation framework has been supplemented with an implementation road-map. Goal models and process models have completely different objectives and characteristics. The most crucial differential characteristic being the sequence-agnostic nature of goal models. In this perspective, it becomes necessary to spell out a mechanism for semantic effect annotation of goal models, and how these effects can be reconciled over the entire enterprise for performing different kinds of analysis.
The main motivation of the research is to help designers and developers identify and rectify errors in the requirements phase itself, even before the requirements are formally documented and specified.
Department of Computer Science & Engineering, University of Calcutta, India