[BBH+19] Nathalie Bertrand, Benjamin Bordais, Loïc Hélouët, Thomas Mari, Julie Parreaux and Ocan Sankur. Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking. In Proc. 3rd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail'19), Springer. 2019. [Uses probabilistic model checking and PRISM to formally evaluate the performance of regulation algorithms in metro train lines.]
Notes: The original publication is available at link.springer.com.