UPPAAL’s Languages and Philips’ Bounded Retransmission Protocol
UPPAAL’s Modeling and Specification Language
Timed Automata
Timed Safety Automata = Timed Automata + Invariants
Networks of Timed Automata
Timed Automata in UPPAAL
Declarations in UPPAAL
Urgent Channels
Urgent Locations
Committed Locations
UPPAAL Specification Language
Philips Bounded Retransmission Protocol
Protocol Overview
Overview of BRP
How It Works
BRP Model Overview
The Lossy Media
Bounded Retransmission
Process S
Process R
The Sender and Receiver
Today’s Lab Assignments
E-post: paupet@docs.uu.se
Hemsida: http://www.docs.uu.se/~paupet/gu/rts/