Formal Test Automation: The Conference Protocol with PHACT

We discuss a case study of automatic test generation and test execution based on formal methods. The case is the Conference Protocol, a simple, chatbox-like protocol, for which (formal) specifications and multiple implementations are publicly available and which is also used in other case study experiments. The tool used for test generation and test execution is Phact, the PHilips Automated Conformance Tester. The formal method is (Extented) Finite State Machines which is the input language for Phact. The experiment consists of developing a Finite State Machine specification for the Conference Protocol, generating 82 tests in TTCN with Phact, and executing these tests against 28 different implementations of the Conference Protocol, both correct and erroneous ones. The result is that some erroneous implementations are not detected by the test cases. These results are analysed, the merits of Extented Finite State Machines for specification are discussed, and the achievements of Phact are assessed. Moreover, the results are compared with a previous experiment in which the same 28 implementations were tested based on specifications in LOTOS and Promela