Protocol testing - Finite State Machine and test generation

Question

Recently, I've been reading about formal methods of network protocol testing. I needed to make that research for my thesis and basically I've got no hands-on experience on methods described in IEEE documents.

The interesting part is about automatic generation of test cases. I must mention that I was working on an automatic validation tool for DHCPv6 protocol (the link, if you care) and every test case I wrote manually.

Most of documents I've found are pretty old (92' - example). Basically, what I understood is (please correct me if I am missing something, that would appreciated):

1. Given a specification document (RFC for example), create a Finite State Machine model based on the specification
2. Generate tests by applying some method (TT (Transition Tour), D, UIO) to the FSM model created in step 1
3. Parameterize test cases - assign input data and expected output data

ad. 1 - In what language would I model a FSM, SDL (what about TTCN)? Is this really worth doing? I know that the larger the protocol, the more effort is needed to make a solid FSM, but what are the pros of this way over writing tests manually?
ad. 2 - how would I traverse created FSM?

If there's anyone who had ever done such things, please share your experiences.

Answer 1

If you haven't already, search for "model-based testing". To me it seems that your problem fits well to that scheme: create a model of expected behaviour and let the testing tool run millions of tests to check the implementation.

This doesn't actually prove anything. Formal validation needs to explicitly go through all paths (as far as I know). Model-based testing just helps generating a lot of different paths. Additionally any problems with the model cause either parts not being tested in the software or false positive errors.