3

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.

4
  • Not a complete answer, but 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. AFAIK this is not really formal in a way of proving the behaviour of the system under test, but anyway could give you much better coverage of the whole.
    – Edu
    Oct 20, 2014 at 10:01
  • I second Edu's comment about model-based testing. It has some good tools for dealing with your questions about generating the model and traversing it.
    – Bruce
    Oct 24, 2014 at 21:52
  • While I haven't done a lot of this type of testing, I imagine its advantage over manual test case generation is in the level of confidence obtained. When you manually create test cases, you never really know what important case you've missed - and inevitably, there are some. Within the limits of model-based testing (ie, the extent the model actually matches reality, etc), it can give you assurances like "there is no set of input messages to DHCPv6 that will return data the caller shouldn't see." (I don't know enough about DHCPv6 to know if that actually makes sense. :) )
    – Bruce
    Oct 24, 2014 at 21:57
  • why not making answers out of your comments? I got some useful information from reading about model-based testing and got a big picture of whole process.
    – macfij
    Oct 26, 2014 at 20:54

1 Answer 1

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.

3
  • Bounty has expired :/ Could elabor a little bit more about the part that it is not really formal way of proving system correctness?
    – macfij
    Oct 28, 2014 at 12:54
  • No problem with the bounty. :-) I update the answer a little.
    – Edu
    Oct 28, 2014 at 13:13
  • I agree with you. Basically, using model-based testing doesn't provide covering all system behaviours. The implemented model could miss something. I am eager to say that validating a system could be done properly with unit tests or tests generated by model. Those two are just different approaches.
    – macfij
    Oct 28, 2014 at 14:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.