This page contains models of a wireless networks based on the 802.11p MAC protocols for Vehicular ad-hoc networks (VANETS). The models are developed using the Symmetric Stochastic Net formalism, which is a coloured stochastic Petri net kind of formalism. The models are given the .grml format which is readable by the COSMOS statistical model checker. A property specification is also given in term of the Hybrid Automata Specification Language (HASL), i.e. by means of an .lha file which represents a Linear Hybrid Automaton that can be used with COSMOS to compute throughput measures for the VANETS models.
802.11pOneMedium.grml: the Symmetric Stochastic Net (coloured stochastic Petri net) model representing a 1-hop network of N stations using 802.11p MAC to for sending data over a shared (ideal) channel
802.11pOneMediumNoisy.grml: the Symmetric Stochastic Net (coloured stochastic Petri net) model representing a 1-hop network of N stations using 802.11p MAC to for sending data over a shared faulty channel (a channel which periodically is affected by error bursts)
throughput.lha: an Linear Hybrid Automaton (LHA) that can be used to estimates the throughput for successful transmissions of data packets at different level of priority