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):
- Given a specification document (RFC for example), create a Finite State Machine model based on the specification
- Generate tests by applying some method (TT (Transition Tour), D, UIO) to the FSM model created in step 1
- 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.