Formal Test Automation: The Conference Protocol with PHACT

A.W. Heerink, Hasan Ural (Editor), Robert L. Probert (Editor), J. Feenstra, G.J. Tretmans, Gregor von Bochmann (Editor)

    Research output: Contribution to conferencePaperpeer-review

    153 Downloads (Pure)


    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.
    Original languageUndefined
    Number of pages10
    Publication statusPublished - 2000
    Event13th IFIP International Conference on Testing Communicating Systems, TestCom 2000 - Ottawa, Canada
    Duration: 29 Aug 20001 Sept 2000
    Conference number: 13


    Conference13th IFIP International Conference on Testing Communicating Systems, TestCom 2000
    Abbreviated titleTestCom


    • IR-66991
    • Conformance testing
    • Case Study
    • Formal Methods
    • finite state machines
    • EWI-9477
    • test execution
    • test generation

    Cite this