The paper describes an approach that bridges the gap between early requirements specifications and formal methods. In particular, we propose a new specification language, called Formal Tropos, that offers the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) [YU97], but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, and in particular model checking, to allow for an automatic verification of relevant properties of the early requirements specification. Our preliminary experiments show that formal analysis reveals gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis tools
Model Checking Early Requirements Specifications in Tropos
Pistore, Marco;Mylopoulos, John;Traverso, Paolo
2001-01-01
Abstract
The paper describes an approach that bridges the gap between early requirements specifications and formal methods. In particular, we propose a new specification language, called Formal Tropos, that offers the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) [YU97], but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, and in particular model checking, to allow for an automatic verification of relevant properties of the early requirements specification. Our preliminary experiments show that formal analysis reveals gaps and inconsistencies in early requirements that are by no means trivial to discover without the help of formal analysis toolsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
