The UML and Formal Methods: a Case Study