Analysis software for model checking Edinburgh buses

  • Daniel Reijsbergen (Creator)
  • Wulinjian Gao (Creator)



This software is supplementary material for the paper 'An automated methodology for analysing urban transportation systems using model checking' by Daniƫl Reijsbergen and Stephen Gilmore. It was used to construct the figures and tables of the paper. In general, its main purpose is to use a dataset of GPS traces of urban transportation vehicles to 1) obtain a route map in the form of an image file and a more abstract graph representation, 2) automatically obtain a patch structure representing stages of the route, and 3) use the patch structure to build a simulation model that can be used to evaluate the punctuality of the underlying transportation service. In particular, it makes use of the dataset available at

Data Citation

Reijsbergen, Daniel; Gao, Wulinjian. (2016). Analysis Software for Model Checking Edinburgh Buses, [software]. University of Edinburgh. School of Informatics..
Date made available1 Sept 2016
PublisherEdinburgh DataShare
Temporal coverage2016 - 2016
Geographical coverageEdinburgh

Cite this