Text this: Protocol specification, testing, and verification, IV :