Data networking has not been kind to formal methods. The Internet's birth gave rise to an intense culture war between the bell-heads and the net-heads, which the net-heads have largely won. In this area formal methodists have long been seen as the humourless enforcers of the defeated bell-heads. The result: formal methods are not a part of the mainstream of data networking and are largely relegated to the the thankless task of reverse engineering (security-related protocols are perhaps the rare exception). If we want to move beyond this situation we must build tools that enhance the ability to engage in the Internet culture | tools that encourage community-based development of open-source systems and embrace the open-ended exploration of design spaces that are only partially understood.
2
If Internet protocols are not developed from formal speci cations it may still be worthwhile to reverse engineer existing protocols. I've done a lot of reverse engineering with routing protocols. I think it can be very fruitful, especially if we can come away with general principles that have applicability beyond protocol-speci c details. This last point is very important | your results must be interesting to a larger community because you can't expect the networking community to care. By the time you have gured something out, they will have moved on to a new set of problems. 3
Given the cultural constraints, perhaps reverse engineering is the best we can do. Attempts have
been made to lower the cost of formal methods, see the work on lightweight formal methods [
I'll suggest one answer | domain-speci c languages (DSLs). It seems to me that DSLs
allow us to raise the level of abstraction in which problems are solved. I will discuss only three
examples | the Statecall Policy Language (SPL) [
I've had fun discussing this topic with Anil Madhavapeddy, Jon Crowcroft, and Boon Thau Loo. I hope this short talk will stimulate further discussion at the ATE workshop.