Abstract: The character of the bimodal multicast is introduced with an example. Formal specification of the bimodal multicast is discussed. A formal specification of bimodal multicast based on IOA is presented, mainly including the definition of the action and state space of the bimodal multicast and the description of the message. The description of the random semantic is also discussed, with emphasis on the "most recent first" os the bimodal multicast.

Key words: bimodal multicast, I/O automata, formal specification, most recent first