Subject: Re: [edu-team] CPN Tools

From: Marc Petit-Huguenin <[email-masked]>
Date: Sat, 31 Aug 2013 09:53:10 -0700

Hi Brian,

On 08/29/2013 01:35 PM, Brian E Carpenter wrote:
> 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.

Well, that's true for any question presented to the IETF list, right?  But my
suggestion was not to ask the community if they want or not to use such tool,
but more about showing how this tool can help publish better protocols, and
let people make their mind.  Information, not new process.

> 
> 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.

Reading this document, it seems to me that the Mealy machines were put in the
draft more to document the protocol than because they were the basis of a
formal approach.  But that brings me to another of my pet peeve, incorrect
examples in RFC.  I think that it should be possible to automatically generate
examples (either textual examples like SIP messages or ladder diagrams) from a
CPN model, especially with CPN Tools as it supports writing this kind of
extension (My credit in the acknowledgment section of RFC 6544 was because I
wrote the tools to automatically generate the examples)

> 
> 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*.

Yes, I realize now that the only tools that are part of the tutorial series
are the tools to prepare internet-drafts and meetecho, all success stories.

> 
> 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.

That's a good suggestion, but I do not think that there is enough people
knowing about CPN Tools at the IETF to even organize that yet.  If I had the
money I would sponsor a table at the next bit-n-bites to show demos, but
that's not an option.

So I think I'll start with Richard suggestion, which is to do some reviews
using CPN Tools, although I will start with an existing RFC instead of a
protocol under development, as that would cut on the argument that the tool
did not find any problem that would not have been found by a traditional
review before publication.

> 
> (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.)

Right, although CPN and SAN are used for different goals.

> 
> [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

Thanks.

> 
> On 29/08/2013 05:24, Marc Petit-Huguenin wrote: 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.
> 
>>>> 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] <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,
>>>> 
>>>> I think Coloured Petri Nets and more specifically the free tool CPN
>>>> Tools (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.
>>>> 
>>>> 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: Radia Perlman <[email-masked]>
Date: Tue, 3 Sep 2013 12:12:13 -0700

Or possibly, after (as Brian puts it) a "real success story with an IETF
protocol", introducing the notion (not with details) at a plenary first,
together with the impact made by using it on a real protocol, and then
perhaps have a tutorial.  Just doing a tutorial first...I'd think it might
be too esoteric, and people wouldn't know why they should be interested.

Radia

On Thu, Aug 29, 2013 at 1:35 PM, Brian E Carpenter <
[email-masked]> wrote:

> 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.)
>
> 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.
> Regards
>    Brian Carpenter
> On 29/08/2013 05:24, Marc Petit-Huguenin 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.
> >
> > 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.
> >
> >> I've copied the EDU team, since they would probably be the most natural
> >> folks to organize such a tutorial.
> >>
> >> Cheers, --Richard
> >>
> >>
> >>
> >>
> Aug
> >> 28, 2013 at 12:16 PM Subject: CPN Tools To: Gonzalo Camarillo
> >> <[email-masked] <mailto:[email-masked]
> >>,
> >> "Richard L. Barnes" <[email-masked]>
> >>
> >>
> >> Hi,
> >>
> Tools
> >> (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.
> >>
> >> 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
> >> 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).
> >>
> >> [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]
> > -----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-----
> > _______________________________________________
> > edu-team mailing list
> > [email-masked]
> > https://www.ietf.org/mailman/listinfo/edu-team
> >
> _______________________________________________
> edu-team mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/edu-team
>