Customer Reviews

Design And Validation Of Computer Protocols

5 star:		(2)
4 star:		(2)
3 star:		(1)
2 star:		(0)
1 star:		(0)

 

 

You have probably read the text from the back cover of the book, which is cited above. Every word of it is true. This is an excellent book, even for (serious) beginners, but also for experts who need some advice on how to avoid bad designs.

All in all it is a joy to read this book as a thorough introduction to the subject. But I have to mention some criticism:

1. Holzmann did the research for the book in the late 1980s and the book was copyrighted in 1991. Therefore some parts look a bit dated now.

2. This is probably one of the best books on the design of network protocols. But who designs protocols ? Do you intend to specify a new protocol ? Probably not. For all those mere mortals who just want to have a quick look at the basics of network protocol, this book is probably too much material. And I am afraid, those few people who do indeed design protocols might take it as a weakness of the book that it does not focus on their favourite protocol family. Instead, Holzmann shows them how to design and verify (!) the correctness of completely new protocols.

3. Network protocols have a long history ! Still today we can learn from historical prototypes. Their basics can be traced back hundreds of years and it is a joy to see how Holzmann mentions them again and again even in the later (more formal) chapters.

It's clear that this book is a little bit outdated compared to Holzmann's recent book on the SPIN model checker. However, i feel that the SPIN book does not explain how difficult it is to design even very simple protocols. In this one, Holzmann provides examples of protocols that look really simple while proving their correctness is utterly difficult. The examples are of particular interest for people working in networking.

The interest of this book is mainly historical, since it treats protocol standardization and the design problems in early computer protocols. The latter half of the book presents the Promela language and the associated SPIN model checker, both of which are far better presented in the recent book "The SPIN model checker" by the same author (hence only the four stars since half of the book is now outdated).

I read this book on Japanese translated version.
The book is good translated.
I whold recommend all of network programmer should read this book.

History of network protocol and model checking is good for stady.
We can understand why we should check a protocol and we should make a model.

SPIN and promela is good tool for programmer.
If you interest in SPIN and promela, new book should be readed.

BTW, c programs for some checksum on the Japanese translated book are little different from this latest English book. I will report this for Japanese translators who are well known network protocol designers.

It turns out to be as much user manual for a validation tool, which is ok. I'd been hoping to use it to check a complicated protocol for a product I was building, but couldn't make any progress in a month. Partly this is my own inadequacy, partly its a problem of applying formal methods to real-world cases, and partly its a problem of examples that are too simple (reflecting the problems of formal methods).

On the other hand, the description of race conditions in the introductory material is lucid, and if you haven't designed in and debugged a few of those, you might find it valuble. A bit pricey for that, though.

It is an excellent book that combines both the aspects - design as well as validation of computer protocols. It covers both the areas in a very neat and succinct fashion.