nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Proving the Safety of a Sliding Window Protocol with Event-B

verfasst von : Sophie Coudert

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

This paper presents an Event-B modeling of the general version of the Sliding Window Protocol (SWP). SWPs ensure reliable data transfer over unreliable media by routing frames together with their indexes. Providing SWPs with formal guarantees is recognized to be quite complex. The experiment we present here shows that Event-B refinement is a suitable approach to ensure the safety of the protocol. First a simple model is developed with unbounded frame indexes. Then bounded indexes and modular arithmetic are introduced, as concrete indexes have fixed size. At this “hybrid” level, unbounded indexes are not used any more in computations but they are still useful to express some properties. Finally, abstract general media are refined towards queues, as an example of implementation. All unbounded indexes fully disappear in the final model.

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 Verifying System-Level Security of a Smart Ballot Box

Nächstes Kapitel Event-B Formalization of Event-B Contexts

https://perso.telecom-paristech.fr/coudert/downloads/SWProdin3_5v1.zip.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-77543-8_4/503576_1_En_4_IEq42_HTML.gif

restricts the domain of function F to S.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-77543-8_4/503576_1_En_4_IEq43_HTML.gif

restricts it to \(dom(F)\backslash S\).

Notice that frame outside the receiver window may be too old or too recent ones.

We are currently transposing them in the new release of the Rodin theory plugin.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-77543-8_4/503576_1_En_4_IEq138_HTML.gif

becomes

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-77543-8_4/503576_1_En_4_IEq139_HTML.gif

later in refinement.

Reminder: acknowledgments outside the window are handled by event reack.

Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRef

Stenning, N.V.: A data transfer protocol. Comput. Netw. 1(2), 99–110 (1976)

Tanenbaum, A.S., et al.: Computer Networks. Prentice-Hall (1996)

Richier, J.-L., Rodriguez, C., Sifakis, J., Voiron, J.: Verification in XESAR of the sliding window protocol. In: IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, NLD. North-Holland Publishing Co (1987)

Kaivola, R.: Using compositional preorders in the verification of sliding window protocol. In: Grumberg, O. (ed.) CAV 1997. LNCS, pp. 48–59. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_8

Godefroid, P., Long, D.E.: Symbolic protocol verification with queue BDDs. Formal Methods Syst. Des. 14(3), 257–271 (1999)

Smith, M.A., Klarlund, N.: Verification of a sliding window protocol using IOA and MONA. In: FORTE/PSTV 2000, pp. 19–34. NLD (2000). Kluwer, B.V

Chkliaev, D., Hooman, J., de Vink, E.: Verification and improvement of the sliding window protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 113–127. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_9CrossRefMATH

Badban, B., Fokkink, W., Groote, J.F., Pang, J., van de Pol, J.: Verification of a sliding window protocol in \(\mu \)CRL and PVS. Formal Aspects Comput. 17(3), 342–388 (2005)

10.

Siala, B., Bhiri, M.T., Bodeveix, J.-P., Filali, M.: An event-B development process for the distributed BIP framework. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 313–328. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_20CrossRef

11.

Stankaitis, P., Iliasov, A., Ait-Ameur, Y., Kobayashi, T., Ishikawa, F., Romanovsky, A.: A refinement based method for developing distributed protocols. In: HASE 2019, pp. 90–97 (2019)

12.

Event-B home page. http://www.event-b.org/

13.

Zhu, C., Butler, M., Cirstea, C.: Trace semantics and refinement patterns for real-time properties in Event-B models. Sci. Comput. Program. 197 (2020)

14.

Sulskus, G., Poppleton, M., Rezazadeh, A.: An interval-based approach to modelling time in event-B. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 292–307. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_20CrossRef

15.

Rusu, V.: Verifying a sliding-window protocol using PVS. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IIFIP, vol. 69, pp. 251–268. Springer, Boston, MA (2002). https://doi.org/10.1007/0-306-47003-9_16CrossRef

16.

Chkliaev, D., Nepomniaschy, V.: Deductive verification of the sliding window protocol. Autom. Control. Comput. Sci. 47, 12 (2013)

17.

Fokkink, W., Pang, J., De Pol, J.: Cones and foci: A mechanical framework for protocol verification. Form. Methods Syst. Des. 29(1), 1–31 (2006)CrossRef

18.

Van de Snepscheut, J.L.A.: The sliding-window protocol revisited. Formal Aspects Comput. 7(1), 3–17 (1995)CrossRef

19.

Hoogerwoord, R.R.: A formal derivation of a sliding window protocol. Computer science reports. Technische Universiteit Eindhoven (2006)

20.

Méry, D.: Modelling by patterns for correct-by-construction process. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 399–423. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03418-4_24CrossRef

21.

Butler, M.: Incremental design of distributed systems with Event-B. Eng. Methods Tools Softw. Saf. Secur. 22(131) (2009)

22.

Silva, R., Butler, M.: Shared event composition/decomposition in event-B. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 122–141. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_7CrossRef

Titel: Proving the Safety of a Sliding Window Protocol with Event-B
verfasst von: Sophie Coudert
Verlag: Springer International Publishing
Buch: Rigorous State-Based Methods
Print ISBN: 978-3-030-77542-1

Electronic ISBN: 978-3-030-77543-8

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-77543-8_4

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"

Premium Partner