[irtf-discuss] Usable formal methods side meeting at IETF 115

[Colin Perkins <[e-mail]>]

Hi,

How should we describe and specify protocols?

How can we ensure that network protocol specifications are consistent 
and correct, and verify that implementations match the specification?

The IETF community has long used natural language, English, to describe 
and specify its protocols, with occasional use of formal languages and a 
some limited amounts of formal verification. One of the sessions in the 
Applied Networking Research Workshop at IETF 114 [1] started to discuss 
whether this is the right approach, and to what extent formal methods, 
structured specification languages, and natural language processing 
techniques can help describe network protocols.

Chris Wood and I are organising a side meeting at IETF 115 to continue 
this discussion, and to assess interest in forming a new IRTF research 
group to explore usable formal methods for protocol specification.

This will takes place on Thursday lunchtime, 10 November, from 
11:30-13:00 UK time in room Richmond 5 of the IETF meeting hotel (the 
IAB breakout room).

The draft agenda is as follows:

   - Welcome, Goals, Motivation, Introductions
       - (15 mins)
   - Short presentations (45 mins)
       - “What are Formal Methods and Why Should We Care?”Jonathan 
Hoyland
       - “Formal Specification and Specification-Based Testing of 
QUIC”, Ken McMillan
   - Discussion of proposed charter (20 mins)
       - See [Google 
Doc](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#)
   - Next steps (10 mins)
       - Does this seem appropriate for an RG?
       - Are there volunteers to work on this topic?
       - What, if anything, have we missed?

if you’re interested in this topic, please review [the draft 
charter](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#) 
and come along to the side meeting to give your feedback.

Hope to see you in London!

Colin



[1] https://www.youtube.com/watch?v=tCsiB87s-f4

-- 
Colin Perkins
https://csperkins.org/