Specyfikacja protokołu alternującego bitu (Alternating Bit Protocol) w języku Estelle:

specification ABtmout systemactivity;

timescale seconds;

const tmout=2;

channel TR(M,A);
  by M:
    Msg(data: integer; 
        bit: integer);
  by A:
    Ack(ack: integer);

module Sender activity;
  ip comm: TR(M) individual queue;
end;
module Loosy activity;
  ip commT: TR(A) individual queue;
     commR: TR(M) individual queue;
end;
module Rec activity;
  ip comm: TR(A) individual queue;
end;

body SenderB for Sender;

  state S1, S2, S3;
  var m, s: integer;

  initialize to S2
      begin
        s := 0
      end;
  trans 
    from S1 to S2
      begin 
        { next message generating }
      end;
  trans
    from S2 to S3
       begin
	 output comm.Msg(m,s);
       end;
  trans 
    from S3 to S1 when comm.Ack 
      provided (ack = s)
        begin
          s:=1-s;
        end; 
  trans 
    from S3 to S2 when comm.Ack 
      provided ( ack <> s )
        begin end; 
  trans 
    from S3 to S2 delay(tmout)
        begin end; 

end; { SenderB }

body ReceiverB for Rec;    

  state R1, R2, R3;
  var i,a,e: integer;

  initialize to R2
        begin 
          e:=0                  
        end;

  trans 
    from R1 to R2
	begin 
          { message accepting}
        end;
  trans 
    from R2 to R3 when comm.Msg
        begin
	  i:=data;
          a:=bit;
	  output comm.Ack(a);
        end;

  trans 
    from R3 to R1 provided (a = e)
        begin
          e:=1-e;
        end;

  trans
    from R3 to R2 provided (a <> e)  
        begin end;

end; { ReceiverB }

body LoosyChanB for Loosy;

  state C1;

  initialize to C1
         begin end;
  trans
    from C1 to same when commT.Msg
         begin output commR.Msg(data,bit) end;
  trans
    from C1 to same when commT.Msg
         begin end;
  trans                          
    from C1 to same when commR.Ack
         begin output commT.Ack(ack) end;
  trans                          
    from C1 to same when commR.Ack
          begin end;

end; { LoosyChanB }

modvar
  S: Sender;
  C: Loosy;
  R: Rec;

    initialize
      begin
        init S with SenderB;
        init C with LoosyChanB;
        init R with ReceiverB;
        connect S.comm to C.commT;
        connect C.commR to R.comm;
       end;
end.