Portal de Periódicos da CAPES

Verification with real-time COSPAN

1993; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-56496-9_22

1611-3349

Costas Courcoubetis, David L. Dill, M. Chatzaki, P. Tzounakis,

Embedded Systems Design Techniques

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).