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 conferencePaperAcademicpeer-review

    63 Downloads (Pure)

    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.
    Original languageUndefined
    Pages211-220
    Number of pages10
    Publication statusPublished - 2000
    EventIFIP TC6/WG6.1 13th International Conference on Testing Communicating Systems: Tools and Techniques, TESTCOM 2000 - Ottawa, Canada
    Duration: 29 Aug 20001 Sep 2000

    Conference

    ConferenceIFIP TC6/WG6.1 13th International Conference on Testing Communicating Systems: Tools and Techniques, TESTCOM 2000
    Period29/08/001/09/00
    OtherAugust 29 - September 1, 2000

    Keywords

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

    Cite this