Abstract:

The network computing model is theoretically deep and scientifically
fundamental, and it led to a range of revolutionary technologies
from global communication to real time software control of complex
systems.  However, every aspect of work on network computing would
benefit from a more abstract logical account of it.

This talk presents very informally an abstract account of network
computing that arose out of our work on specifying, optimizing and
verifying distributed protocols -- work we did jointly with the
systems group at Cornell (Ken Birman, Robbert Van Renesse and
students).  In this account, formal specifications are very readable
and natural.  The logic of events is quite simple, and in it we can
prove that specifications are achievable.  Such demonstrations can
be used to guide correct-by-construction process synthesis, and they
are also compact explanations of why a process is correct.  We will
illustrate this method on a very simple example and mention our
current work in this logic of events.

This is joint work with my colleague Mark Bickford of the ATC-NY
Corporation who is applying it to real systems.