LOTOS(language of temporal ordering specification) is a protocol specification language based on process algebra CCS. It is geared to protocol verification, but it is not powerful enough for describing some properties of practical protocols. This paper introduces a language ELOTOS(extended LOTOS), with the power of describing asynchronous communication, time, and stochastic event occurring.