The first protocols were specified in a sort of structured
English - text. This is very difficult to check for anything.
Flowcharting has been used, but is an unnatural framework for
specifying concurrency, and leads to very large charts. It
does, however allow for some automatic checking and generating
of parts of a protocol.
More powerful techniques are:
State Diagrams - like Markov Diagrams.
Very useful to humans, but get large and not machine readable.
A variety of state transition graphs, can help check protocols,
but not intuitive for human implementor.
Grammers :- Backus Naur Form.
Can be bent to describe formats and sequences of actions in a
protocol, and is well known by programmers. Not so useful for
checking for concurrency problems.
Format and Protocol languages.
These are most promising for the future.