Verification with real-time COSPAN

Abstract

We describe some examples using an extension of Kurshan’s COSPAN system to verify bounded delay constraints in a dense time model, based on the method proposed by Dill for adding timing constraints to Büchi automata. The S/R model and COSPAN are reviewed as background, then we describe how timing can be incorporated into S/R processes, and briefly describe the modified verification algorithm. The examples consist of several time-dependent versions of the Alternating Bit Protocol and the Fiber Distributed Data Interface (FDDI).