i*ToNuSMV: A Prototype for Enabling Model Checking of i* Models
Novarun Deb, Nabendu Chaki, Aditya Ghose · 2016
Goal model like i* are inherently sequence agnostic whereas standard model checkers like SPIN or NuSMV accept extended finite state models which represent an ordering of state transitions that can occur within a system. These two notions are mutually conflicting and, thus, we cannot check temporal properties (like compliance rules), described using temporal languages (like Linear Temporal Logic (LTL), or Computational Tree Logic (CTL)), on goal models by feeding them as input to a standard model checker. The i*ToNuSMV tool aims to bridge this gap such that the compliance of i* models towards temporal constraints can be verified in the early requirements phase of software development itself.