A modular approach to formal specification and verification of dependable distributed protocols