Proceedings Fifth IEEE International Symposium on Requirements Engineering (2001)
Aug. 27, 2001 to Aug. 31, 2001
Ariel Fuxman , University of Toronto
John Mylopoulos , University of Toronto
Marco Pistore , ITC-IRST
Paolo Traverso , ITC-IRST
Abstract: This paper describes an attempt to bridge the gap between early requirements specification and formal methods. In particular, we propose a new specification language, called Formal Tropos, that is founded on the primitive concepts of early requirements frameworks (actor, goal, strategic dependency) , but supplements them with a rich temporal specification language. We also extend existing formal analysis techniques, in particular model checking, to allow for an automatic verification of relevant proper-ties for an early requirements specification. Our preliminary experiments demonstrate 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.
M. Pistore, A. Fuxman, J. Mylopoulos and P. Traverso, "Model Checking Early Requirements Specifications in Tropos," Proceedings Fifth IEEE International Symposium on Requirements Engineering(RE), Toronto, Canada, 2001, pp. 0174.