Skip to main content
placeholder image

i*ToNuSMV: A Prototype for Enabling Model Checking of i* Models

Conference Paper


Abstract


  • © 2016 IEEE.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.

UOW Authors


  •   Deb, Novarun (external author)
  •   Chaki, Nabendu (external author)
  •   Ghose, Aditya

Publication Date


  • 2016

Citation


  • Deb, N., Chaki, N. & Ghose, A. (2016). i*ToNuSMV: A Prototype for Enabling Model Checking of i* Models. 2016 IEEE 24th International Requirements Engineering Conference (RE) (pp. 397-398). United States: IEEE Xplore.

Scopus Eid


  • 2-s2.0-85007275980

Start Page


  • 397

End Page


  • 398

Abstract


  • © 2016 IEEE.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.

UOW Authors


  •   Deb, Novarun (external author)
  •   Chaki, Nabendu (external author)
  •   Ghose, Aditya

Publication Date


  • 2016

Citation


  • Deb, N., Chaki, N. & Ghose, A. (2016). i*ToNuSMV: A Prototype for Enabling Model Checking of i* Models. 2016 IEEE 24th International Requirements Engineering Conference (RE) (pp. 397-398). United States: IEEE Xplore.

Scopus Eid


  • 2-s2.0-85007275980

Start Page


  • 397

End Page


  • 398