Specifying and Analyzing Early Requirements: Some Experimental Results

Formal Tropos is a specification language for early requirements. It is based on concepts from an agent-oriented early requirement model framework (i*) and extends them with a rich temporal specification language. In earlier work, we demonstrated through a small case study how model checking could be used to verify early requirements written in Formal Tropos. In this paper we address issues of methodology and scalability for our earlier proposal. In particular, we propose guidelines for producing a Formal Tropos specification from an i* diagram and for deciding what model checking technique to use when a particular formal property is to be validated. We also evaluate the scope and scalability of our proposal using a tool, the T-Tool, that maps Formal Tropos specifications to a language that can be handled by NuSMV, a state-of-the-art model checker. Our experiments are based on a course management case study