Re: [hackathon] Formal Languages at the Hackathon

[Carsten Bormann <[e-mail]>]

I’m sharing the below with t2trg as it appears to be highly related to some of our current work.

I’d also like to point out that formal description techniques (FDT) have been used a lot at the IETF and the IRTF:

* we know very well how to use ABNF (RFC 5234) for our text-based protocols.  We don’t really have a good way to work with multiple layers of ABNF, though; see the difference between RFC 5988 and RFC 8288 for some recent improvements (but the link between the layers is not formal).  ABNF tools exist for both checking ABNF specs and for automatically generating instances (examples).

* specific areas have had their FDTs, e.g. RFC 4997 for ROHC, YANG for management, etc.  Specifically YANG is increasingly used not only for its original purpose, describing management information bases, but also for data on the wire (yang-data).  YOUPI [1] is an interesting YANG extension for describing arbitrary binary data.

[1]: https://tools.ietf.org/html/draft-petrov-t2trg-youpi

* some RFCs were to a large extent machine-generated text (e.g., RFC 7400) or machine-verified (e.g., RFC 8428), based on models in various FDTs.  Some of these are very domain-specific, but we could still be better on sharing tools (and long-term preserving the sources that generated those RFCs).

* there is a lively discussion about adding (structural) data modeling (a.k.a. “schemas”) to JSON over at the mailing list of the closed JSON WG (e.g., [2]).  While that discussion is ongoing, we already have CDDL (RFC 8610) for structurally modeling CBOR and JSON data.  Maybe one size does not fit all here.  Similar to ABNF, CDDL tools can check specs, verify instances against a spec, extract/generate code snippets from specs, and generate instances/examples from specs.  One next step here is adding links to application semantics.

[2]: https://tools.ietf.org/html/draft-ucarion-jddf

* the WISHI activity in T2TRG looks at modeling data shapes, interaction modeling, and potentially adding protocol bindings towards the wire and application semantics towards the application.  Several SDOs are providing interesting study subjects, e.g., W3C WoT with their Thing Description (TD) [3] and the still somewhat stealthy OneDM group with the Simple Definition Format (SDF) [4].  We’ll discuss this on the Friday before the IETF [5] and work on tools for it at the Hackathon (look for “WISHI”).

[3]: https://www.w3.org/TR/wot-thing-description/
[4]: https://github.com/one-data-model/language/blob/master/sdf.md
[5]: https://github.com/t2trg/2019-11-singapore
(Yes, you can still register.)

I understand that the “Formal Languages” activity mostly addresses their use in IETF specifications, and I like that angle — there are other uses of formal description techniques that possible have a different set of requirements, which sometimes cause the requirements of spec writers to be forgotten [6].

[6]: https://www.iab.org/wp-content/IAB-uploads/2016/03/Noise-in-specifications-hurts.pdf

So I’m really looking forward to the discussions on Friday, November 15th [5] and at the Hackathon.  Getting something going on cross-pollinating and coordinating the various FDT activities at IETF and IRTF might be a good medium term goal.

Grüße, Carsten



> On Nov 6, 2019, at 11:09, Stephen McQuistin <[e-mail]> wrote:
> 
> Hi all,
> 
> Marc Petit-Huguenin and I are championing formal languages projects at the hackathon in Singapore. Broadly, these
> projects seek to improve the quality of standards by using formal and structured languages in specification documents.
> These documents can then be parsed by tooling that can, for example, generate parser code or verify properties for the
> protocol being specified.
> 
> There will be two formal languages projects being worked on: Augmented Packet Header Diagrams and Computerate
> Specifying. Details for both projects are available on the Wiki at https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages,
> but I'll give a brief outline of the Augmented Packet Header Diagrams project here. I'll let Marc describe his
> Computerate Specifying project separately.
> 
> The Augmented Packet Header Diagram format (draft-mcquistin-augmented-ascii-diagrams) is a consistent packet header
> diagram format and accompanying structured text constructs that allow for the parsing process of protocol headers to be
> fully specified. This provides support for the automatic generation of parser code, and for other benefits that follow
> from being able to use tooling to process packet header diagrams.
> 
> Our goal at the hackathon is to improve both the Augmented Packet Header Diagram format itself, by attempting to rewrite
> existing I-Ds and RFCs using its syntax, and to improve the tooling, and in particular, its Rust parser generator.
> 
> Please join us: we are particularly interested in examples of packet header diagrams that might be challenging to write
> in the format our draft describes, and in how our tooling might fit into existing workflows.
> 
> I-D: https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams
> Getting started information: https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages
> 
> Thanks,
> 
> Stephen
> 
> 
> 
> _______________________________________________
> hackathon mailing list
> [e-mail]
> https://www.ietf.org/mailman/listinfo/hackathon