This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.

In this paper, a construction of de Bruijn sequences using maximum length linear sequences is considered. The construction is based on the well-known cross-join (CJ) method: Maximum length linear sequences are used to produce de Bruijn sequences by the CJ process. Properties of the CJ paris in the maximum length linear sequences are investigated. It is conjectured that the number of CJ pairs in a maximum length linear sequence is given by (22n-3+1)/3-2n-2, where n2 is the length of the linear feedback shift register with the sequence. The CJ paris for some special cases are obtained. An algorithm for finding CJ pairs is described and a method of implementation is discussed briefly.