Industrial practices in requirements engineering do not give the right place to formal methods. Two main reasons explain why such a failure arises. First of all, formal methods have not promoted a dedicated SLC (software life cycle) which should have been easily integrated within the upper phases of the traditional V-like or Waterfall-like model. A second reason is that formal methods have failed in scaling up. We show how the requirements elicitation phase can take advantage of formal methods. We report the industrial and successful experience (D. Gianazza et al., 1997) undertaken by the STNA, a governmental office responsible for the French ATM (air traffic management) system. We exhibit the evolutionary model which was applied to develop both a validated object oriented model of a particular ATM subsystem, and a formal specification of some of its safety critical parts. We then show that the SRD (Software Requirements Document) is the key of the whole development. Its writing requires a strongly related cooperation of two different teams that are effective actors of the evolutionary model. We conclude the paper by presenting some recommendations.