Path: utzoo!utgpu!water!watmath!clyde!bellcore!faline!thumper!karn
From: karn@thumper.bellcore.com (Phil R. Karn)
Newsgroups: comp.protocols.tcp-ip
Subject: Re: TCP-IP Verification Suite
Summary: is formal TCP/IP verification needed?
Message-ID: <922@thumper.bellcore.com>
Date: 2 Feb 88 19:32:51 GMT
References: <7011@ihlpa.ATT.COM> <8802011551.AA06681@ishmael.cray.com>
Organization: Bell Communications Research, Inc
Lines: 24

> The TCP/IP community does not have a strong tradition of formal
> testing from specifications.  Historically (see RFC-1025, ``TCP and IP
> Bake Off''), testing a TCP/IP implementation has meant structured
> plugging it in and trying it, with as many other implementations as
> possible.

Actually, I think there is a lot to be said for this approach.  Formal
verification is difficult, slow and expensive, while the informal
testing of a new implementation on the real Internet quickly shows
whether it's likely to work in actual use.  The real world has a way of
revealing things that remain stubbornly hidden in the lab.

The TCP/IP experience has shown that finding clear-cut protocol
violations is not difficult. The *real* issues are

a) getting rid of gaps and ambiguities in the specs themselves that can
allow different implementations to "conform" yet not be interoperable, and

b) figuring out how to armtwist the vendor of a broken implementation to
fix it once a problem has been identified.

Formal verification suites attack neither of these problems.

Phil