Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Leveraging Applications of Formal Methods

ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems pp 274–287Cite as

Data-Driven Modelling and Simulation of Urban Transportation Systems Using Carma

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11246))

Abstract

Public transportation systems of different degrees and complexity are widely employed in cities around the world. Well-organised and efficient public transportation reduces traffic and the time spent commuting to work. In addition, more people choosing public transport rather than personal cars has a positive impact on reducing the number of vehicles on city roads: lessening their effect on climate change, improving air quality, and reducing noise pollution. Modelling and simulation of urban transportation systems is one way of analysing the influence that a variety of factors have on the overall functioning of the system. In this paper we present a Collective Adaptive Systems (CAS) model of an urban transportation system. We compare aspects of real data collected from a city bus system in the city of Edinburgh, UK, with the results of simulations of the CAS model constructed in the carma language. The simulations show results which are in good agreement with the real-world data, leading us to believe that the model could have useful predictive powers and thus provide an environment for experimentation with possible changes to the design of the system.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Reijsbergen, D., Gilmore, S.: Formal punctuality analysis of frequent bus services using headway data. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 164–178. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10885-8_12

    Chapter  Google Scholar 

  2. Katoen, J.-P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), pp. 31–45 (2016)

    Google Scholar 

  3. Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunĉak, V. (eds.) Computer Aided Verification. CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

  4. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  5. Bortolussi, L., et al.: CARMA: collective adaptive resource-sharing Markovian agents. In: Proceedings of Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems, (QAPL 2015), vol. 194, pp. 16–31. EPTCS (2015)

    Google Scholar 

  6. Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 83–119. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_4

    Chapter  Google Scholar 

  7. Nicola, R.: A formal approach to autonomic systems programming: the SCEL language. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 24–28. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15317-9_2

    Chapter  Google Scholar 

  8. Abd Alrahman, Y., De Nicola, R., Loreti, M.: On the power of attribute-based communication. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 1–18. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_1

    Chapter  Google Scholar 

  9. Hillston, J., Loreti, M.: CARMA eclipse plug-in: a tool supporting design and analysis of collective adaptive systems. In: Agha, G., Van Houdt, B. (eds.) Quantitative Evaluation of Systems, QEST 2016. LNCS, vol. 9826. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_12

  10. Transport for Edinburgh Ltd. http://transportforedinburgh.com/

  11. Lothian Buses. https://lothianbuses.co.uk/

  12. GitHub repository of scripts used for data handling. https://github.com/nataliazon/LothianBusesScripts/

  13. Tom Tom Traffic Flow for Edinburgh. https://www.tomtom.com/en_gb/traffic-news/edinburgh-traffic/traffic-flow/

  14. Tom Tom Traffic News. https://www.tomtom.com/en_gb/traffic-news/

  15. Vissat, L.L., Clark, A., Gilmore, S.: Finding optimal timetables for Edinburgh bus routes. Electron. Notes Theor. Comput. Sci. 310, 179–199 (2015)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Edinburgh, Scotland

    Natalia Zon & Stephen Gilmore

Authors
  1. Natalia Zon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stephen Gilmore
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Natalia Zon .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zon, N., Gilmore, S. (2018). Data-Driven Modelling and Simulation of Urban Transportation Systems Using Carma. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. ISoLA 2018. Lecture Notes in Computer Science(), vol 11246. Springer, Cham. https://doi.org/10.1007/978-3-030-03424-5_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03424-5_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03423-8

  • Online ISBN: 978-3-030-03424-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation