Abstract: The automatic transition from requirements definition to formal specification is an important problem in requirements engineering. Based on the requirements definition language NDRDL and the specification language Z, this paper discusses a transformation method from NDRDL to Z, with emphasis on how to get state space and operation definition in Z from requirements definition in NDRDL.