Istituto di Scienza e Tecnologie dell'Informazione     
Mazzanti F., Spagnolo G. O., Ferrari A. Designing a deadlock-free train scheduler: a model checking approach. In: NFM 2014 - NASA Formal Methods. 6th International Symposium (Houston, TX, USA, 29 April - 1 May 2014). Proceedings, vol. 8430 pp. 264 - 269. Julia M. Badger, Kristin Yvonne Rozier (eds.). (Lecture Notes in Computer Science, vol. 8430). Springer, 2014.
In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC.
URL: http://link.springer.com/chapter/10.1007%2F978-3-319-06200-6_22
DOI: 10.1007/978-3-319-06200-6_22
Subject Deadlock
D.2.2 Software Engineering. Design Tools and Techniques
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional