Derivation of Executable Code from Formal Protocol Specifications Written in LOTOS