{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:26:47Z","timestamp":1743071207741,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031231186"},{"type":"electronic","value":"9783031231193"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-23119-3_13","type":"book-chapter","created":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T16:06:51Z","timestamp":1673280411000},"page":"179-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Generating SPARK from\u00a0Event-B, Providing Fundamental Safety and\u00a0Security"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0508-3066","authenticated-orcid":false,"given":"Asieh","family":"Salehi Fathabadi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2196-2749","authenticated-orcid":false,"given":"Dana","family":"Dghaym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4095-0732","authenticated-orcid":false,"given":"Thai Son","family":"Hoang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4642-5373","authenticated-orcid":false,"given":"Michael","family":"Butler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0210-0983","authenticated-orcid":false,"given":"Colin","family":"Snook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,10]]},"reference":[{"key":"13_CR1","unstructured":"Galois and Free & Fair. The BESSPIN Voting System (2019). https:\/\/github.com\/GaloisInc\/BESSPIN-Voting-System-Demonstrator-2019. Accessed 16 Aug 2022"},{"key":"13_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"13_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transfer"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1017\/9781009181358.045","volume-title":"Bibliography","author":"J Barnes","year":"2022","unstructured":"Barnes, J.: Bibliography, 2nd edn., pp. 951\u2013952. Cambridge University Press, Cambridge (2022). https:\/\/doi.org\/10.1017\/9781009181358.045","edition":"2"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/11767077_7","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2006","author":"D Curtis","year":"2006","unstructured":"Curtis, D.: SPARK annotations within executable UML. In: Pinho, L.M., Gonz\u00e1lez Harbour, M. (eds.) Ada-Europe 2006. LNCS, vol. 4006, pp. 83\u201393. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11767077_7"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-030-77543-8_3","volume-title":"Rigorous State-Based Methods","author":"D Dghaym","year":"2021","unstructured":"Dghaym, D., Hoang, T.S., Butler, M., Hu, R., Aniello, L., Sassone, V.: Verifying system-level security of a smart ballot box. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 34\u201349. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_3"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Eysholdt, M., Behrens, H.: Xtext: implement your language faster than the quick and dirty way. In: OOPSLA, pp. 307\u2013309. ACM (2010). http:\/\/doi.acm.org\/10.1145\/1869542.1869625","DOI":"10.1145\/1869542.1869625"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-030-77543-8_12","volume-title":"Rigorous State-Based Methods","author":"A Salehi Fathabadi","year":"2021","unstructured":"Salehi Fathabadi, A., Snook, C., Hoang, T.S., Dghaym, D., Butler, M.: Extensible record structures in Event-B. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 130\u2013136. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_12https:\/\/eprints.soton.ac.uk\/448194\/"},{"key":"13_CR9","unstructured":"Georgiou, K., Cluzel, G., Butcher, P., Moy, Y.: Security-hardening software libraries with Ada and SPARK - a TCP stack use case. CoRR abs\/2109.10347 (2021). https:\/\/arxiv.org\/abs\/2109.10347"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Snook, C., Dghaym, D., Fathabadi, A.S., Butler, M.: Building an extensible textual framework for the Rodin platform. In: Proceedings of the 7th Workshop on Formal Integrated Development Environment, F-IDE2022, to be published","DOI":"10.1007\/978-3-030-77543-8_11"},{"issue":"3","key":"13_CR11","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MS.2013.43","volume":"30","author":"Y Moy","year":"2013","unstructured":"Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or formal verification: do-178c alternatives and industrial experience. IEEE Softw. 30(3), 50\u201357 (2013). https:\/\/doi.org\/10.1109\/MS.2013.43","journal-title":"IEEE Softw."},{"key":"13_CR12","unstructured":"Murali, R., Ireland, A.: E-SPARK: automated generation of provably correct code from formally verified designs. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012)"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Sautejeau, X.: Modeling SPARK systems with UML. In: SigAda 2005, pp. 11\u201316. Association for Computing Machinery, New York (2005). https:\/\/doi.org\/10.1145\/1103846.1103848","DOI":"10.1145\/1103846.1103848"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition tool for Event-B. Softw. Pract. Experience 41(2), 199\u2013208 (2011). https:\/\/eprints.soton.ac.uk\/271714\/","DOI":"10.1002\/spe.1002"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-030-63461-2_6","volume-title":"Integrated Formal Methods","author":"S Sritharan","year":"2020","unstructured":"Sritharan, S., Hoang, T.S.: Towards generating SPARK from Event-B models. In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 103\u2013120. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_6"},{"key":"13_CR16","unstructured":"Wilkie, I.: Executable UML and SPARK Ada: the best of both worlds (2005). https:\/\/abstractsolutions.co.uk\/wp-content\/uploads\/2018\/03\/Executable-UML-and-SPARK-Ada-V2.1.pdf"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-66197-1_2","volume-title":"Software Engineering and Formal Methods","author":"Z Zhang","year":"2017","unstructured":"Zhang, Z., Robby, Hatcliff, J., Moy, Y., Courtieu, P.: Focused certification of an industrial compilation and static verification toolchain. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 17\u201334. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_2"}],"container-title":["Communications in Computer and Information Science","Advances in Model and Data Engineering in the Digitalization Era"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-23119-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T19:11:08Z","timestamp":1673291468000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-23119-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031231186","9783031231193"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-23119-3_13","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"10 January 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MEDI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model and Data Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cairo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Egypt","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"medi2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.medi22.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"65","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.25","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}