In [GJ01], one describes an experiment in verifying 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, maintaining and modifying 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 verification experiment. The results obtained give some hints concerning a methodology for the formal verification of real systems.