In this text and CD-ROM, the major techniques for formally supported specification, design and verification of large programs and complex systems are applied to a non-trivial and non-academic problem which is typical for industrial informal requirements specifications.