Stejným způsobem jako jsme vytvořili sítě DataMedium a AckMedium v předchozí sekci, vytvoříme síť Sender. V ní popíšeme model vysílače.
Vysílač se synchronizuje s hodinami při každém vyslání zprávy a reaguje opětovným vysláním téže zprávy na time-out, jímž hodiny signalizují uplynutí určité doby. Proces Sender tedy modelujeme jako paralelní kompozici procesů Timer (představujícího hodiny) a SenderDef (proces vlastního vysílače). Předpokládejme, že hodiny již máme vymodelované jako síť Timer uloženou v souboru 'timer.net'. Tuto síť načteme pomocí příkazu Import menu Net.
Síť Sender popisující tuto kompozici je zobrazena na obrázku . Zbývá zapsat CCS popis podsystému rozhraní SenderDef (viz obrázek
).
Figure: Specifikace systémů Sender a Timer
Figure: Specifikace procesu SenderDef
Přijímač (Receiver) se také synchronizuje s hodinami, před vysláním potvrzovací zprávy. Specifikujeme jej podobně jako systém Sender (viz obrázky a
).
Figure: Specifikace systému Receiver
Figure: Specifikace procesu ReceiverDef