nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Towards Generating SPARK from Event-B Models

verfasst von : Sanjeevan Sritharan, Thai Son Hoang

Erschienen in: Integrated Formal 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 approach to generate SPARK code from Event-B models. System models in Event-B are translated into SPARK packages including proof annotations. Properties of the Event-B models such as axioms and invariants are also translated and embedded in the resulting models as pre- and post-conditions. This helps with generating SPARK proof annotations automatically hence ensuring the correct behaviour of the resulting code. A prototype plug-in for the Rodin has been developed and the approach is evaluated on different examples. We also discuss the possible extensions including to generate scheduled code and data structures such as records.

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 An Event-B Based Generic Framework for Hybrid Systems Formal Modelling

Nächstes Kapitel Jaint: A Framework for User-Defined Dynamic Taint-Analyses Based on Dynamic Symbolic Execution of Java Programs

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

Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)CrossRef

AdaCore. GNAT Reference Manual, 21.0w edition, July 2020. http://docs.adacore.com/live/wave/gnat_rm/html/gnat_rm/gnat_rm.html

Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, Boston (2003)

Booch, G., Bryan, D.: Software Engineering with ADA, 3rd edn. Addison-Wesley, Boston (1993)MATH

Butler, M.: Reasoned modelling with Event-B. In: Bowen, J., Liu, Z., Zhang, Z. (eds.) SETSS 2016. LNCS, vol. 10215, pp. 51–109. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-56841-6_3CrossRef

Cataño, N., Leino, K.R.M., Rivera, V.: The EventB2Dafny rodin plug-in. In: Garbervetsky, D., Kim, S. (eds.) Proceedings of the 2nd International Workshop on Developing Tools as Plug-Ins, TOPI 2012, Zurich, Switzerland, 3 June 2012, pp. 49–54. IEEE Computer Society (2012)

Dalvandi, M., Butler, M., Rezazadeh, A., Salehi Fathabadi, A.: Verifiable code generation from scheduled Event-B models. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 234–248. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_16CrossRef

Fathabadi, A.S., Snook, C., Hoang, T.S., Dghaym, D., Butler, M.: Extensible data structures in Event-B (submitted to iFM2020)

10.

Hoang, T.: Appendix A: an introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211–236. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-33170-1_1 CrossRef

11.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef

12.

Rustan, K., Leino, M.: Developing verified programs with Dafny. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, p. 82. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27705-4_7CrossRef

13.

Murali, R., Ireland, A.: E-SPARK: automated generation of provably correct code from formally verified designs. Electron. Commun. EASST 53, 1–15 (2012)

14.

Rivera, V., Cataño, N.: Translating Event-B to JML-specified Java programs. In: Cho, Y., Shin, S.Y., Kim, S.-W., Hung, C.-C., Hong, J. (eds.) Symposium on Applied Computing, SAC 2014, Gyeongju, Republic of Korea, 24–28 March 2014, pp. 1264–1271. ACM (2014)

15.

Silva, R., Pascal, C., Hoang, T.S., Butler, M.J.: Decomposition tool for Event-B. Softw. Pract. Exp. 41(2), 199–208 (2011)CrossRef

16.

Snook, C., et al.: Behaviour-driven formal model development. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 21–36. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_2CrossRef

17.

Sritharan, S.: Automated translation of Event-B models to SPARK proof annotations. Technical report, University of Southampton (2020). https://eprints.soton.ac.uk/444034/

18.

thyssenkrupp: MULTI - a new era of mobility in buildings. https://www.thyssenkrupp-elevator.com/uk/products/multi/. Accessed July 2020

Titel: Towards Generating SPARK from Event-B Models
verfasst von: Sanjeevan Sritharan
Thai Son Hoang
Verlag: Springer International Publishing
Buch: Integrated Formal Methods
Print ISBN: 978-3-030-63460-5

Electronic ISBN: 978-3-030-63461-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-63461-2_6

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