PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Franco M., Ferrari A., Spagnolo G. O. Experiments in formal modelling of a deadlock avoidance algorithm for a CBTC system. In: ISoLA 2016 - Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium (Corfu, Greece, 10-14 October 2016). Proceedings, vol. II pp. 297 - 314. Tiziana Margaria, Bernhard Steffen (eds.). (Lecture Notes in Computer Science, vol. 9953). Springer International Publishing, 2016.
 
 
Abstract
(English)
This paper presents a set of experiments in formal modelling and verification of a deadlock avoidance algorithm of an Automatic Train Supervision System (ATS). The algorithm is modelled and verified using four formal environment, namely UMC, Promela/SPIN, NuSMV, and mCRL2. The experience gained in this multiple modelling/verification experiments is described. We show that the algorithm design, structured as a set of concurrent activities cooperating through a shared memory, can be replicated in all the formal frameworks taken into consideration with relative effort. In addition, we highlight specific peculiarities of the various tools and languages, which emerged along our experience.
URL: http://link.springer.com/chapter/10.1007/978-3-319-47169-3_22
DOI: 10.1007/978-3-319-47169-3_22
Subject Formal methods
Train Scheduling
Deadlock Avoidance
Model Checking
Railway
D.2.10 SOFTWARE ENGINEERING. Design
D.2.10 SOFTWARE ENGINEERING. Methodologies
D.2.4 SOFTWARE ENGINEERING. Software/Program Verification
D.2.4 SOFTWARE ENGINEERING. Model checking


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