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

Specifying and Analyzing Early Requirements: Some Experimental Results

Pistore, Marco;Roveri, Marco;Mylopoulos, John
2003-01-01

Abstract

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
2003
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/839
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact