Subject: Re: [edu-team] CPN Tools

From: Richard Barnes <[email-masked]>
Date: Wed, 28 Aug 2013 13:07:23 -0400

Hey Marc,

This sounds interesting.  Even if there's not a tutorial, if there are some
people who are skilled with these tools, they might be able to provide some
uniquely valuable document reviews.

I've copied the EDU team, since they would probably be the most natural
folks to organize such a tutorial.

Cheers,
--Richard

---------- Forwarded message ----------
From: Marc Petit-Huguenin <[email-masked]>
Date: Wed, Aug 28, 2013 at 12:16 PM
Subject: CPN Tools
To: Gonzalo Camarillo <[email-masked]>, "Richard L. Barnes"
<[email-masked]>

Hi,

I think Coloured Petri Nets and more specifically the free tool CPN Tools
(www.cpntools.org) should be used by more protocol designers at the IETF,
so I
would like to propose either a presentation or a tutorial from the current
developer of CPN Tools to the community at a future IETF meeting.

Coloured Petri Net[1] (CPN) is an extension of Petri Net that permits to
construct models of concurrent systems and analyze their properties.  CPN
Tools is a set of tools (a CPN graphical design tool, a simulator, etc...)
that are distributed under FOSS licenses (GPL/LGPL/BSD)[2].  This tools are
useful to verify the design of communication protocols and, according to the
developer of CPN Tools, were used to check and fix errors in DYMO (Dynamic
on-demand routing in MANETs) and IOTP (Internet open trading protocol)
before
publication.  There was even a published analysis[3] on SIP that showed that
the problems in the state machines could have being discovered with CPN
Tools.
 The web site contains more example of CPN models[4] of IETF protocols.

For all these reasons, I believe that a presentation or tutorial about CPN
Tools would be very helpful for the IETF community.  I exchanged emails with
the developer of CPN Tools (Michael Westergaard[5]), and he is interested in
doing such presentation (I was thinking that London would be ideal, as he is
based in Amsterdam, Netherlands).

So would the IETF be interested in this?

Thanks.

[1]
http://www.amazon.com/Coloured-Petri-Nets-Validation-Concurrent/dp/3642002838
[2] http://cpntools.org/download
[3] Liu, L. (2009). Verification of the SIP Transaction Using Coloured Petri
Nets. In Proc. Thirty-Second Australasian Computer Science Conference (ACSC
2009), Wellington, New Zealand. CRPIT, 91. Mans, B., Ed. ACS. 63-72.
[4] http://cpntools.org/documentation/examples/start
[5] http://scholar.google.com/citations?user=LvlZyFwAAAAJ&hl=en

- --
Marc Petit-Huguenin
Email: [email-masked]
Blog: http://blog.marc.petit-huguenin.org
Profile: http://www.linkedin.com/in/petithug

---

From: Richard Barnes <[email-masked]>
Date: Wed, 28 Aug 2013 13:30:58 -0400

On Wed, Aug 28, 2013 at 1:24 PM, Marc Petit-Huguenin <
[email-masked]> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA256
>
> On 08/28/2013 10:07 AM, Richard Barnes wrote:
> > Hey Marc,
> >
> > This sounds interesting.  Even if there's not a tutorial, if there are
> > some people who are skilled with these tools, they might be able to
> provide
> > some uniquely valuable document reviews.
>
> Yes, that's a good idea, although a full analysis of a protocol takes much
> more time than a review (well, I guess it depends on the review), but [1]
> provides some data on the work done by Ericsson Telebit on ERDP,  It took
> 70
> person-hours to do the modeling and 30 hours for the state space analysis
> (after 6 hours of training).  Obviously not something that
> can be done on a voluntary basis for each protocol produced by the IETF,
> unless there is some kind of sponsorship.
>

Good point, and good data.  I would think, though, that if this tool were
shown to have value, you might be able to get some IETF participants to
sponsor.

You might talk to Paul Hoffman.  He's done a lot of interop testing work,
e.g., with VPNs and firewalls.  Robert Sparks could provide some insight
from a SIPit angle, and might have some contacts at UNH IOL (another likely
implementor/sponsor).

Hope this helps,
--Richard

> > Cheers, --Richard
> > ---------- Forwarded message ---------- From: *Marc Petit-Huguenin*
> > <[email-masked] <mailto:[email-masked]>> Date: Wed,
> Aug
> > 28, 2013 at 12:16 PM Subject: CPN Tools To: Gonzalo Camarillo
> > <[email-masked] <mailto:[email-masked]
> >>,
> > "Richard L. Barnes" <[email-masked]>
> >
> >
> > Hi,
> >
> > (www.cpntools.org <http://www.cpntools.org>) should be used by more
> > protocol designers at the IETF, so I would like to propose either a
> > presentation or a tutorial from the current developer of CPN Tools to the
> > community at a future IETF meeting.
> >
> > useful to verify the design of communication protocols and, according to
> > the developer of CPN Tools, were used to check and fix errors in DYMO
> > (Dynamic on-demand routing in MANETs) and IOTP (Internet open trading
> > protocol) before publication.  There was even a published analysis[3] on
> > SIP that showed that the problems in the state machines could have being
> > discovered with CPN Tools. The web site contains more example of CPN
> > models[4] of IETF protocols.
> >
> > Tools would be very helpful for the IETF community.  I exchanged emails
> > with the developer of CPN Tools (Michael Westergaard[5]), and he is
> > interested in doing such presentation (I was thinking that London would
> be
> >  ideal, as he is based in Amsterdam, Netherlands).
> >
> > [3] Liu, L. (2009). Verification of the SIP Transaction Using Coloured
> > Petri Nets. In Proc. Thirty-Second Australasian Computer Science
> Conference
> > (ACSC 2009), Wellington, New Zealand. CRPIT, 91. Mans, B., Ed. ACS.
> 63-72.
> > [4] http://cpntools.org/documentation/examples/start [5]
> > http://scholar.google.com/citations?user=LvlZyFwAAAAJ&hl=en
> >
> >
>
> - --
> Marc Petit-Huguenin
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.14 (GNU/Linux)
>
> iQIcBAEBCAAGBQJSHjJPAAoJECnERZXWan7ExmYP/2gIydfshbQvgUzK5bUkC+qB
> 08GPjsFHthtOZdT9Xik3yS3awlyo3aWc2pC0hRubhJTD1aqerN2cs5Z5a5l1qSnO
> kXujSXArgTHbwB3VQ6jyUeCUhgrBXGxJCdqY+vvssGVVK64/x8w5YJnIWzqtZ3/t
> Mel4COMo2qGa/wzL0JZ0UjLdjlrnaez+suqlC0jVmCxwm928Dz2DvbbsAb9lzZLl
> 3ZxLzYZZ/AFVnWzhc1bo0KMf1a+1+KgGHSlIMGGtvKXbw8etx+QTzhtUVHphA90d
> BBhMAmj+SnQfQiGF3uxAnd9OENSZcZ1ti5fywvJrTZExaGclhjGEl5JwKRXN2BWd
> f2WUuBT6MzVOnl0neE1BpDwRaIoWX67Wzn7q8Axk5sMVwu+Gjom4fogX9H6wkSOT
> MA1y2IhchI4Yd20xHbzIDz6IlDROILmzKocxr7qzQmbOSg49OsF6aVJ9vJyBSOQl
> dwkGJ+QND/Oo/6LROL8cqtrfx1ctKH/qOS9ktaaNdKC8xrCdyEE8+LUgM858TcTM
> mtecfNgOsGL+lPYIxTEL66mo92t8aD5DW+sRIp+WkW3Q0jCtXp3p1vwGVxwlUTAc
> TP3lJXnGe8sgsS0TE27beNj8GSFZpBbiJhnmsXMY+da2XVoLZAmUILVLnmK12Gl9
> Dtjo3VBBZBKlXvHYuem/
> =Dv+o
> -----END PGP SIGNATURE-----
>

---

From: Marc Petit-Huguenin <[email-masked]>
Date: Wed, 28 Aug 2013 10:24:34 -0700

On 08/28/2013 10:07 AM, Richard Barnes wrote:
> some people who are skilled with these tools, they might be able to provide

provides some data on the work done by Ericsson Telebit on ERDP,  It took 70

> <[email-masked] <mailto:[email-masked]>> Date: Wed, Aug 
> <[email-masked] <mailto:[email-masked]>>, 
> interested in doing such presentation (I was thinking that London would be
> Petri Nets. In Proc. Thirty-Second Australasian Computer Science Conference
> (ACSC 2009), Wellington, New Zealand. CRPIT, 91. Mans, B., Ed. ACS. 63-72.

- -- 
Marc Petit-Huguenin

---

From: Brian E Carpenter <[email-masked]>
Date: Fri, 30 Aug 2013 08:35:19 +1200

Hi,

I suspect that if you took this question to the IETF list,
you would find very strong opinions both for and against this
(or any) formal technique for protocol analysis and design.

As it happens, wearing my Gen-ART hat, I have just reviewed
a massive document, draft-ietf-mediactrl-call-flows, that
relies on a semi-formal model (a form of Mealy automaton,
and if you don't know what that is, you can look it up in
Wikipedia like I had to). So there are people in the IETF
willing to apply such methods.

Wearing my EDU hat, I think we could make a case for an
"official" tutorial if there was already at least one real
success story *within the IETF*.

What I would suggest is for those interested to organise
a hands-on workshop, on the Saturday before or after an
IETF. Take a couple of significant IETF protocols and model
them. Prove in public that the method works. A report on such
a workshop would be a great topic for an IAB plenary, IMHO.

(CPNs aren't the only solution of course. Habib Naderi here in
Auckland had some success using Stochastic Activity Networks
to model aspects of shim6 [1] (and later mptcp) operating at very
large scale. Many people have their own preferred method.)

[1] H. Naderi and B.E. Carpenter, A Performance Study on REAchability Protocol
in Large Scale IPv6 Networks (with H. Naderi), Second International
Conference on Computer and Network Technology (ICCNT 2010), Bangkok,
(April 2010) 28-32. Digital Object Identifier: 10.1109/ICCNT.2010.18.
http://www.cs.auckland.ac.nz/~brian/iccnt2010_reap.pdf

Regards
   Brian Carpenter

On 29/08/2013 05:24, Marc Petit-Huguenin wrote:
> _______________________________________________
> edu-team mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/edu-team
>