Abstract
In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR.
This work was partially supported by the PAR FAS 2007-2013 (TRACE-IT) project and by the PRIN 2010-2011 (CINA) project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ferrari, A., Spagnolo, G.O., Martelli, G., Menabeni, S.: From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions. Int. Journal on STTT, 1–21 (2014)
Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: A model checking approach. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 264–269. Springer, Heidelberg (2014)
Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing, M., Hölzl, M. (eds.) Sensoria Project. LNCS, vol. 6582, pp. 390–407. Springer, Heidelberg (2011)
OMG: Object Management Group, UML Superstructure Specification (2006), http://www.omg.org/spec/UML/2.4.1
ter Beek, M.H., Mazzanti, F., Gnesi, S.: CMC-UMC: A Framework for the Verification of abstract Service-Oriented Properties. In: Proceedings of the 2009 ACM Symposium on Applied Computing, pp. 2111–2117. ACM (2009)
Petersen, E., Taylor, A.: Line Block Prevention in Rail Line Dispatch and Simulation Models. INFOR Journal (21), 46–51 (1983)
Cui, Y.: Simulation-based hybrid model for a partially-automatic dispatching of railway operation. Ph.D. Thesis Universitat Stuttgart (2009)
Mills, R., Pudney, P.: The effects of deadlock avoidance on rail network capacity and performance. In: Hewitt, J. (ed.) MISG: Mathematics in Industry Study Group (2003)
Pachl, J.: Avoiding deadlocks in synchronous railway simulations. In: International Seminar on Railway Operations Modelling and Analysis, pp. 359–369 (2007)
Pachl, J.: Deadlock avoidance in railroad operations simulations. In: PROMET Traffic & Transportation. Number 11-0175, pp. 359–369 (2012)
Mittermayr, R., Blieberger, J., Schöbel, A.: Kronecker Algebra based Deadlock Analysis for Railway Systems. PROMET - Traffic & Transportation 24(5), 359–369 (2012)
Törnquist, J.: Computer-based decision support for railway traffic scheduling and dispatching: A review of models and algorithms. In: 5th Workshop on Algorithmic Methods and Models for Optimization of Railways, p. 659 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A. (2014). Deadlock Avoidance in Train Scheduling: A Model Checking Approach. In: Lang, F., Flammini, F. (eds) Formal Methods for Industrial Critical Systems. FMICS 2014. Lecture Notes in Computer Science, vol 8718. Springer, Cham. https://doi.org/10.1007/978-3-319-10702-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-10702-8_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10701-1
Online ISBN: 978-3-319-10702-8
eBook Packages: Computer ScienceComputer Science (R0)