A conformance testing method for communication protocols modeled as concurrent DFSMs. Treatment of non-observable non-determinism

According to the progress of high-speed networks, many communication protocols are specified as concurrent systems. Such systems can be modeled as concurrent deterministic FSMs (DFSMs). In those protocols, a common input may be taken by some of concurrent DFSMs competitively. In such a case, the global behaviour becomes non-deterministic in general. Conformance testing is typically a black-box testing, i.e. it is based on its specification. Formal methods for deriving conformance test cases are widely recognized as being capable of producing tests with high fault coverage. We propose a conformance testing method based on GWp-method for a sub-class of non-observable non-deterministic FSMs (NFSMs). In this class, the global behaviour of many protocols modeled as concurrent DFSMs can be specified. The proposed method can be used not only for testing NFSMs directly but also for testing concurrent DFSMs whose global behaviour becomes non-observable non-deterministic