The KeY system allows integrated informal and formal development of
 object-oriented Java software. In this paper we report on a major
 industrial case study involving safety-critical software for the
 computation of a particular kind of railway time table used by train
 drivers. Our case study includes formal specification of requirements
 both on the analysis and the implementation level.  Particular
 emphasis in our research is laid on the challenge to make authoring
 and maintenance of formal specifications easier. We demonstrate that
 the technique of specification patterns as implemented in KeY 
 for the language OCL yields significant improvements.