Abstract
Based on initial research to transform a sequence agnostic goal model into a finite state model (FSM) and then checking them against temporal properties (in CTL), researchers have come up with guidelines for generating compliant finite state models altogether. The proposed guidelines provide a formal approach to prune a non-compliant FSM (generated by the Semantic Implosion Algorithm) and generate FSM-alternatives that satisfy the given temporal property. This paper is an extension of the previous work that implements the proposed guidelines and builds a deployment interface called i∗ToNuSMV 3.0. The working of the framework is demonstrated with the help of some use cases. In the end, a comparative study of the performance between the previous and current versions of the Semantic Implosion Algorithm (SIA) with respect to the size of the solution space and the execution times, respectively, has also been presented.
