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 computation of a particular
kind of railway time table used by train drivers. Our case study includes formal
specification of requirements on the analysis and the implementation level.
Particular emphasis in our research is put on the challenge of how authoring and
maintenance of formal specifications can be made easier. We demonstrate that the
technique of specification patterns implemented in KeY for the language
OCL yields significant improvements.