Analysis Software for Model Checking Edinburgh Buses

Abstract

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 https://doi.org/10.7488/ds/1470.