A Hybrid Approach to Formal Verification Applied to an ATM Switching System

Verifying the correctness of real-time system models by traditional approaches that depend on the exploration of the entire system state space is impractical for large systems. In contrast, testing allows the search for violations of a property to be narrowed to a relatively small portion of the overall state space based on assumptions regarding the structure of an implementation. We present a hybrid approach that exploits formal methods to verify subcomponents of a system and testing to gain confidence in the correctness of the assembled system. The feasibility of the approach is demonstrated by application of the method to a process algebra model of the Sunshine ATM switching network.