For complex industrial software systems it is often necessary to add or reimplement components for future releases. This task is not treated with formal methods so far. We show how a formal development technique can be used to develop a specification of an existing distributed system based on a set of allowed sequences of communications taken either from the documentation or from observations of the running system.The main emphasis of the approach is to develop a deadlock-free specification of the system which can be used in the desired ways. The development begins with a description of the typical behaviour which is stepwise extended with more functionality leading to an incremental development technique.An industrial case study (a PABX) is taken as an example to document the applicability of the approach as part of a reengineering technique. It is shown that earlier design steps can be repeated in a formal way as a combination of the incremental development technique with transformation rules which preserve deadlock-freedom.