Uppaal WLAN

Model of a simplified WLAN 802.11p tranceiver application as published in the paper:

Hybrid Latency Minimization Approach using Model Checking and Dataflow Analysis

Guus Kuiper, Philip S. Kurtin, Marco J.G. Bekooij

@inproceedings{kuiper2017hybrid,
  title={Hybrid latency minimization approach using model checking and dataflow analysis},
  author={Kuiper, Guus and Kurtin, Philip S and Bekooij, Marco J G},
  booktitle={Int'l Workshop on Software and Compilers for Embedded Systems (SCOPES)},
  url = {http://dx.doi.org/10.1145/3078659.3078665},
  year={2017},
  organization={ACM}
}

Models

Wlan.xml over-approximates the finish-time of tasks to remain decidable.

WlanSw.xml uses stopwatches, where Uppaal performs over-approximations in the analysis.