[erlang-questions] Quickcheck'ing a protocol

Jesper Louis Andersen <>
Fri Sep 23 09:53:34 CEST 2016

On Thu, Sep 22, 2016 at 10:43 PM, Josh Adams <> wrote:

> This all sounds amazing and like a thing I'd like to encourage the world
> to adopt.

The world seems to agree. A recent news article touches on the subject[0],
where Jeanette Wing (and probably her research group) are working on
building a formal model of TLS.

There are a couple of viable avenues you can adopt. One of the more
promising is to write down a formal specification from which you can derive
test cases. But if constructed correctly, they can also be executed at the
same time. Erlang isn't a nice vehicle for this since you are lack
(Standard) ML style functors, but the ideas are certainly transferable.

Because you can also execute the model, you can use it as a driver in a
QuickCheck test case and make sure that some other implementation is
correct w.r.t to the executable specification.

The way to approach this kind of thing is to crawl before walking. Start
out with a small ping-pong protocol which base64 encodes its queries and
responses. Then show this correct and use that to build gradually more
complex stuff. Most of the full quickcheck developments starts in a corner
of the full system and then gradually extend themselves. Trying to attack a
full system from day 1 is usually hard.

Also, you have to learn some tricks in order to handle standard protocol
problems. By targeting toys with those problems it is often easier to
figure out how to handle them, before trying to do it on the full system.
Model building is fun, but it takes the same thought process as when you
are trying to solve an abstract math problem: the answer will come to you
why you are doing other stuff, muddling on the question.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20160923/cf5c63a8/attachment.html>

More information about the erlang-questions mailing list