Formal Test Automation: The Conference Protocol with PHACT


Heerink, Lex and Feenstra, Jan and Tretmans, Jan (2000) Formal Test Automation: The Conference Protocol with PHACT. In: IFIP TC6/WG6.1 13th International Conference on Testing Communicating Systems: Tools and Techniques, TESTCOM 2000, August 29 - September 1, 2000, Ottawa, Canada (pp. pp. 211-220).

open access
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:© 2000 Kluwer Academic
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 120879