We describe an attempt to bridge the gap between earlyrequirements specification and formal methods. In particular, we proposea new specification language, called Formal Tropos, that is founded onthe primitive concepts of early requirements frameworks (actor, goal,strategic dependency) (Yu, 1997), but supplements them with a richtemporal specification language. We also extend existing formal analysistechniques, in particular model checking, to allow for an automaticverification of relevant properties for an early requirementsspecification. Our preliminary experiments demonstrate that formalanalysis reveals gaps and inconsistencies in early requirements that areby no means trivial to discover without the help of formal analysistools
展开▼
