W. Glasgow-subway,

B. Adeline, P. Dersin, E. Fabre, L. Hélouët, and K. Kecir, An efficient evaluation scheme for KPIs in regulated urban train systems, Reliability, Safety, and Security of Railway Systems (RSSRAIL'17), pp.195-211, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01646919

C. Baier and J. Katoen, Principles of model checking, 2008.

G. Behrmann, A. David, and K. G. Larsen, , 2006.

V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker, Automated verification techniques for probabilistic systems, Formal Methods for Eternal Networked Software Systems (SFM'11), vol.6659, pp.53-113, 2011.
DOI : 10.1007/978-3-642-21455-4_3

URL : https://hal.archives-ouvertes.fr/hal-00648037

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.6, issue.5, pp.512-535, 1994.
DOI : 10.1007/bf01211866

A. E. Haxthausen and J. Peleska, Formal development and verification of a distributed railway control system, IEEE Trans. Software Eng, vol.26, issue.8, pp.687-701, 2000.

M. Kettner, B. Sewcyk, and C. Eickmann, Integrating microscopic and macroscopic models for railway network evaluation, Association for European Transport, 2003.

H. N. Koustopoulos and Z. Wang, Simulation of urban rail operations: model and calibration methodology, Transport Simulation, Beyond Traditional Approaches, pp.153-169, 2009.

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of probabilistic real-time systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), vol.6806, pp.585-591, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00648035

A. Nash and D. Huerlimann, Railroad simulation using opentrack, Computers in Railways IX, pp.45-54, 2004.

, Metro service performance indicators, a UITP information sheet, 2011.

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science FOCS'77, pp.46-57, 1977.