Formal Verification of Abstract System and Protocol Specifications

Formal methods are starting to become more widely used in industry for digital circuit design verification. For this purpose EDA (electronic design automation) tool vendors provide some formal verification solutions on so-called RT-Level. On the other hand the state-of-the-art method to specify functional system and protocol details on a high level of abstraction is textual specification in natural language. Verification is done manually by inspections and implicitly by testing the implementation. Using an example from the telecommunication industry the following case study demonstrates a new methodology to model abstract specifications using model checking. It is shown how typical specification errors can be found in an early stage of system development.