In this paper, we describe a case study on the verification of a real industrial protocol for wireless atm, called mascara. Several tools have been used: sdl has been chosen as the specification language and the commercial tool Objectgeode has been used for creating and maintaining sdl descriptions. The if tool-set has been used for generation, minimization and comparison of system models and verification of expected properties. All specification and verification tools are connected via the if language, which has been defined as an intermediate representation for timed asynchronous systems as well as an open validation environment. Due to the complexity of the protocol, static analysis techniques, such as live variable analysis and program slicing, were the key to the success of this case study. The results obtained give some hints concerning a methodology for the formal verification of real systems.