A. Semenov
A. Yakovlev
N. Anisimov
University of Newcastle upon Tyne. 1995.
A reliable self-timed channel, based on a pipeline ring architecture, uses a special-purpose protocol with prioritised token access. The previous design of a channel adaptor was implemented by speed-independent circuits but without a strict proof of formal correctness of the protocol. Now we are planning to redesign the interface by means of recently developed net-based methods and software tools. This paper presents a compositional technique to construct a labelled Petri net model of this protocol and describes the results of its automatic verification using Pr/T nets.