Constructing automated protocol testing oracles to accommodate specification nondeterminism

The large number of test inputs and outputs usually involved in testing of protocols makes automated output checking necessary. An automated oracle in the test environment achieves this automation. It is imperative that the oracle should be tolerant of nondeterminism in the specifications. This paper presents an and-state method to accommodate specification nondeterminism in automated protocol resting oracles. The and-state method generates concurrent system states when encountering nondeterminism. The and-state method reduces the computational cost of an oracle by avoiding running n concurrent copies of the system to generate all n possible behaviors caused by nondeterminism. We illustrate the and-state method using example specifications given in the Specification and Description Language (SDL). We applied this method to an automated oracle of a small protocol in a network system consisting of 60 nodes. The experimental results show that this oracle facilitates random testing of the protocol