Heh….this reminded me of a project I had to do circa 1991/2 when getting my Master's in EE where we used this book and mechanism to 'validate' TCP. http://spinroot.com/gerard/popd.html
Although as a student homework assignment I wouldn't say what we did was in any way rigorous but certainly had me learning some interesting concepts (and as I was actually creating a backbone with routers at the time it was kind of fun to see where academics and operations went a bit orthogonal) :) And no, I can't for the life of me remember that far back except to remember that I was the only one in class with practical knowledge. And then of course there's the 'how did one actually implement the protocols' and hence the Interop conferences as someone already mentioned. Even a formal proof of 'protocol validation and correctness' doesn't alter the implementation creativities… - merike On Sep 28, 2014, at 11:41 PM, George Michaelson <g...@algebras.org> wrote: > for two asynchronous, otherwise unconnected systems, using TCP/IP there is > a state transition sequence which can be shown to work if you stick to it. > There are also (I believe) corner cases when you send unexpected sequences, > and some of them have known behaviours > > in that sense, the question: "does the RFC adequately document the state > transition sequences which are understood to be valid states and > transitions" is a well formed question. > > Robin Milner, in his calculus of communicating systems tried to codify a > formal mathematics of async communicating systems. I don't know if anyone > either extended the idea(s) or applied it to TCP/IP. > > Certainly I believe there are formally verified protocols. Thats a space > Erlang occupies isn't it? > > On Mon, Sep 29, 2014 at 4:14 PM, Larry Sheldon <larryshel...@cox.net> wrote: > >> On 9/29/2014 00:32, Pete Carah wrote: >> >>> For that matter, has the*specification* of tcp/ip been proven to be >>> "correct" in any complete way? >>> >> >> I find that question in this forum really confusing. >> >> I thought all of the RFC-descriptions of protocols were taken to be >> statements that "if you do it this way, we think we can inter-operate" but >> at no time to be taken as "right" or "wrong". >> -- >> The unique Characteristics of System Administrators: >> >> The fact that they are infallible; and, >> >> The fact that they learn from their mistakes. >> >> >> Quis custodiet ipsos custodes >>
signature.asc
Description: Message signed with OpenPGP using GPGMail
