Automatic generation of formal specification from requirements definition

Developing software on the bases of formal functional specifications in first order logic and algebraic languages has been the prime endeavour of research on formal methods. But, the industrial development community has been slow to adopt formal methods. Instead, researchers and software engineers in the area of software requirements engineering have advanced various notations for defining user´s requirements and systematic methods of developing requirements definitions. There is a wide gap between the current practice of software requirements engineering and the research on formal specification and software formal development. This paper presents the system NDRASS, which supports requirements engineering with the methods of current state of practice and to link such practice to formal methods by automatically generating formal functional specifications in Z.