Interoperability testing is a basic necessity in the case of interconnecting network products
designed to correctly transport information between devices. There are some non-determinisims within a
specification as well as in its implementation. In this paper, the traditional non-determinisim in a specification
is thoroughly analysed, and other features are discussed, based on specifications. In order to describe a
specification more precisely, basic Petri Net is extended to describe new kinds of non-determinisim.
Furthermore, a modelling method that considers the interaction relationship, the non-determinisim and the
ambiguous specification is proposed. An algorithm is introduced to generate a composite model from Petri
Nets and MSC (Message Sequence Chart). Moreover, an algorithm considering optimal test sequence
generation is introduced, based on the reachability graph of the synthesis of a Petri Net. Finally, the
conclusion and suggestions for future research work are given.