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

[Sampo Syreeni <[e-mail]>]

On 2022-11-06, Buday Gergely wrote:

> Formal methods is a broad term, what did people actually suggest?

I'd argue the first thing to do would be to find out which form of 
temporal logic covers every extant IETF protocol. How to marry that then 
with a formal language able to carry all of the data formats used. Once 
you have those, you have a framework at least capable of describing what 
we already have.

What you have might not be ideal for formal methods use. It might 
surface reasoning with all of that would not be efficient. Or your 
framework might not align with any current reasoning software. But 
still, it would constitute a formal defition, at least amenable to 
*some* formal work. Which is more than what we have now.

> Model checking has a long track record of verifying protocols, 
> especially the Spin model checker by Gerald Holzmann.

So, maybe its input language/formalism? [...]

> I think English should augment formal specifications as it could 
> ignite debate whether the formalisation is correct and unambigous.

Here I'd go more with the literal programming idea, and coloring your 
statements with comments. Because if you really formalized your protocol 
fully, so that the formal description really is whole and binding, there 
is no need for debate. It just is or isn't valid.

As such English (why not other languages) simply serve to explain to a 
human, what the intended semantics of the protocol and its data formats 
are meant to be.
-- 
Sampo Syreeni, aka decoy - [e-mail], http://decoy.iki.fi/front
[phone], 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2