A Hybrid Approach to Formal Verification Applied to an ATM Switching System
Duncan L. Clarke, Insup Lee · ScholarlyCommons (University of Pennsylvania) · 1996
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. This research was supported in part by ONR N00014-89-J-1131S1, NSF CCR93-11622, and DARPA/NSF CCR9014621. Contents 1 Introduction 3 2 Algebra of Communicating Shared Resources with Value Passing and its Toolkit 4 2.1 ACSR-VP : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : ...