nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Formal Distributed Protocol Development for Reservation of Railway Sections

verfasst von : Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Yamine Aït-Ameur, Fuyuki Ishikawa, Alexander Romanovsky

Erschienen in: Rigorous State-Based Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The decentralisation of railway signalling systems has the potential to increase railway network capacity, availability and reduce maintenance costs. Given the safety-critical nature of railway signalling and the complexity of novel distributed signalling solutions, their safety should be guaranteed by using thorough system validation methods. In this paper, we present a rigorous formal development and verification of a distributed protocol for reservation of railway sections, which we believe could deliver benefits of a decentralised signalling while ensuring safety and liveness properties. For the formal distributed protocol development and verification, we devised a multifaceted framework, which aims to reduce modelling and verification effort, while still providing complementary techniques to study protocol from all relevant perspectives.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes

Nächstes Kapitel Verifying SGAC Access Control Policies: A Comparison of ProB, Alloy and Z3

A single signalling computer may be responsible for controlling tens of routes (case studies [18, 20]) whereas novel distributed systems would reduce that number.

A complete protocol description and formal models can be found at http://stankaitis.uk/2019/02/.

Instead, of \(\mathsf {ppt}\) upper limit we decided plot the probability against the queue depth, (offset - \(\mathsf {n}\)) as it directly shows how many times an agent can renegotiate resources.

INTO-CPS Project. Case Studies 2, Deliverable D1.2. Technical report, November 2016. http://projects.au.dk/fileadmin/D1.2a_Case_Studies.pdf

Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2013)MATH

Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Météor: a successful application of B in a large project. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_22CrossRef

Bernstein, P.A., Shipman, D.W., Rothnie Jr., J.B.: Concurrency control in a System For Distributed Databases (SDD-1). ACM Trans. Database Syst. 5(1), 18–51 (1980)CrossRef

Cansell, D., Méry, D.: Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm. Theor. Comput. Sci. 364(3), 318–337 (2006)MathSciNetCrossRef

Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating SMT solvers in rodin. Sci. Comput. Program. 94(P2), 130–143 (2014)CrossRef

Essamé, D., Dollé, D.: B in large-scale projects: the canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 252–254. Springer, Heidelberg (2006). https://doi.org/10.1007/11955757_21CrossRef

Eswaran, K.P., Gray, J., Lorie, R.A., Traiger, I.L.: The notions of consistency and predicate locks in a database system. Commun. ACM 19(11), 624–633 (1976)MathSciNetCrossRef

Fantechi, A., Haxthausen, A.E., Nielsen, M.B.R.: Model checking geographically distributed interlocking systems using UMC. In: 25th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP), pp. 278–286, March 2017

10.

Fantechi, A., Haxthausen, A.E.: Safety Interlocking as a distributed mutual exclusion problem. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 52–66. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_4CrossRef

11.

Gray, J., Reuter, A.: Transaction Processing: Concepts and Techniques, 1st edn. Morgan Kaufmann Publishers Inc., San Francisco (1992)MATH

12.

Hawblitzel, C., et al.: IronFleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83–92 (2017)CrossRef

13.

Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 687–701 (2000)CrossRef

14.

Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_29CrossRef

15.

Hoang, T.S., Kuruma, H., Basin, D., Abrial, J.R.: Developing topology discovery in event-B. Sci. Comput. Program. 74(11), 879–899 (2009)MathSciNetCrossRef

16.

Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A.: Formal derivation of a distributed program in event B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 420–436. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_29CrossRef

17.

Iliasov, A., Stankaitis, P., Adjepon-Yamoah, D., Romanovsky, A.: Rodin platform why3 plug-in. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 275–281. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_21CrossRef

18.

Iliasov, A., Taylor, D., Laibinis, L., Romanovsky, A.: Formal verification of signalling programs with SafeCap. In: Gallina, B., Skavhaug, A., Bitsch, F. (eds.) SAFECOMP 2018. LNCS, vol. 11093, pp. 91–106. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99130-6_7CrossRef

19.

Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46CrossRef

20.

Limbrée, C., Cappart, Q., Pecheur, C., Tonetta, S.: Verification of railway interlocking - compositional approach with OCRA. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 134–149. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33951-1_10CrossRef

21.

Morley, M.: Safety assurance in interlocking design. Ph.D. thesis, University of Edinburgh, College of Science and Engineering, School of Informatics (1996)

22.

Newcombe, C.: Why Amazon chose TLA\(^{+}\). In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 25–39. Springer, Berlin (2014). https://doi.org/10.1007/978-3-662-43652-3_3CrossRef

23.

Stankaitis, P., Iliasov, A., Ait-Ameur, Y., Kobayashi, T., Ishikawa, F., Romanovsky, A.: A refinement based method for developing distributed protocols. In: IEEE 19th International Symposium on High Assurance Systems Engineering (HASE), pp. 90–97, January 2019

24.

Whitwam, F., Kanner, A.: Control of automatic guided vehicles without wayside interlocking. Patent US 20120323411, A1 (2012)

Titel: Formal Distributed Protocol Development for Reservation of Railway Sections
verfasst von: Paulius Stankaitis
Alexei Iliasov
Tsutomu Kobayashi
Yamine Aït-Ameur
Fuyuki Ishikawa
Alexander Romanovsky
Verlag: Springer International Publishing
Buch: Rigorous State-Based Methods
Print ISBN: 978-3-030-48076-9

Electronic ISBN: 978-3-030-48077-6

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-48077-6_14

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"