Model checking early requirements specifications in Tropos

@inproceedings{fuxman01, abstract = {We describe 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) (Yu, 1997), 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 properties 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}, address = {Toronto}, author = {Fuxman, A. and Pistore, M. and Mylopoulos, J. and Traverso, P. }, booktitle = {International Symposium on Requirements Engineering}, citeulike-article-id = {819459}, journal = {RE01}, keywords = {evaluation, formal, modeling, temporal}, month = {August}, pages = {174--181}, posted-at = {2006-08-27 20:17:06}, priority = {0}, title = {Model checking early requirements specifications in Tropos}, url = {http://ieeexplore.ieee.org/xpls/abs\_all.jsp?arnumber=948557}, year = {2001} }

TY - CONF ID - fuxman01 L3 - citeulike-article-id:819459 TI - Model checking early requirements specifications in Tropos T2 - International Symposium on Requirements Engineering JF - RE01 SP - 174 EP - 181 AD - Toronto N2 - We describe 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) (Yu, 1997), 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 properties 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 KW - evaluation KW - formal KW - modeling KW - temporal AU - Fuxman, A AU - Pistore, M AU - Mylopoulos, J AU - Traverso, P PY - 2001/08/27--31/ UR - http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=948557 ER -