{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T10:06:33Z","timestamp":1776679593490,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030963071","type":"print"},{"value":"9783030963088","type":"electronic"}],"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.springer.com\/tdm"},{"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.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-96308-8_9","type":"book-chapter","created":{"date-parts":[[2022,3,26]],"date-time":"2022-03-26T13:15:41Z","timestamp":1648300541000},"page":"93-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification Techniques: A Comparative Analysis for Critical System Design"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6607-2707","authenticated-orcid":false,"given":"Rahul","family":"Karmakar","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,27]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574924","volume-title":"The Way of Z: Practical Programming with Formal Methods","author":"J Jacky","year":"1996","unstructured":"Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR2","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings by J. R. Abrial. Cambridge University Press, Cambridge (1726)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, Cambridge (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Karmakar, R., Sarkar, B.B., Chaki, N.: System modeling using Event-B: an insight. In: SSRN Scholarly Paper ID 3511455, Social Science Research Network, Rochester, NY, December 2019","DOI":"10.2139\/ssrn.3511455"},{"key":"9_CR5","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/978-981-15-7834-2_60","volume-title":"Proceedings of International Conference on Frontiers in Computing and Systems","author":"R Karmakar","year":"2021","unstructured":"Karmakar, R., Sarkar, B.B., Chaki, N.: Event-B based formal modeling of a controller: a case study. In: Bhattacharjee, D., Kole, D.K., Dey, N., Basu, S., Plewczynski, D. (eds.) Proceedings of International Conference on Frontiers in Computing and Systems. AISC, vol. 1255, pp. 649\u2013658. Springer, Singapore (2021). https:\/\/doi.org\/10.1007\/978-981-15-7834-2_60"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s42979-020-00412-8","volume":"2","author":"R Karmakar","year":"2021","unstructured":"Karmakar, R., Sarkar, B.B.: A prototype modeling of smart irrigation system using Event-B. SN Comput. Sci. 2(1), 1\u20139 (2021). https:\/\/doi.org\/10.1007\/s42979-020-00412-8","journal-title":"SN Comput. Sci."},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-00255-7_2","volume-title":"Integrated Formal Methods","author":"M Butler","year":"2009","unstructured":"Butler, M.: Decomposition structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 20\u201338. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00255-7_2"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-17071-3_5","volume-title":"Formal Methods for Components and Objects","author":"A Salehi Fathabadi","year":"2010","unstructured":"Salehi Fathabadi, A., Butler, M.: Applying Event-B atomicity decomposition to a multi media protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 89\u2013104. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17071-3_5"},{"issue":"3","key":"9_CR9","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s00165-014-0311-1","volume":"27","author":"AS Fathabadi","year":"2015","unstructured":"Fathabadi, A.S., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Aspects Comput. 27(3), 499\u2013523 (2015)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"9_CR10","doi-asserted-by":"publisher","first-page":"1557","DOI":"10.1007\/s10270-013-0391-z","volume":"14","author":"MY Said","year":"2013","unstructured":"Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model. 14(4), 1557\u20131580 (2013). https:\/\/doi.org\/10.1007\/s10270-013-0391-z","journal-title":"Softw. Syst. Model."},{"key":"9_CR11","unstructured":"Hvannberg, E.: Combining UML and Z in a Software Process (2001)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Sengupta, S., Bhattacharya, S.: Formalization of UML use case diagram-a Z notation based approach. In: 2006 International Conference on Computing & Informatics, pp. 1\u20136, Kuala Lumpur, Malaysia. IEEE, June 2006","DOI":"10.1109\/ICOCI.2006.5276507"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/3-540-45140-4_28","volume-title":"Advanced Information Systems Engineering","author":"S Dupuy","year":"2000","unstructured":"Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An overview of RoZ\u202f: a tool for integrating UML and Z specifications. In: Wangler, B., Bergman, L. (eds.) CAiSE 2000. LNCS, vol. 1789, pp. 417\u2013430. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45140-4_28"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Younes, A.B., Ayed, L.J.B.: Using UML activity diagrams and Event B for distributed and parallel applications. In: 31st Annual International Computer Software and Applications Conference, vol. 1, (COMPSAC 2007), pp. 163\u2013170, Beijing, China. IEEE, July 2007. ISSN: 0730-3157","DOI":"10.1109\/COMPSAC.2007.233"},{"issue":"1","key":"9_CR15","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: formal modelling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-030-47679-3_32","volume-title":"Computer Information Systems and Industrial Management","author":"R Karmakar","year":"2020","unstructured":"Karmakar, R., Sarkar, B.B., Chaki, N.: Event ordering using graphical notation for Event-B models. In: Saeed, K., Dvorsk\u00fd, J. (eds.) CISIM 2020. LNCS, vol. 12133, pp. 377\u2013389. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-47679-3_32"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Halder, A., Karmakar, R.: Mapping UML activity diagrams into Z notation. In: Innovative Data Communication Technologies and Application, Proceedings ICIDCA-2021, Lecture Notes on Data Engineering and Communications Technologies. Springer, Cham (2022). ISSN: 2367-4512","DOI":"10.1007\/978-981-16-7167-8_23"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology - SoICT 2011, p. 179, Hanoi, Vietnam, 2011. ACM Press (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"9_CR19","unstructured":"Steve, W.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-Based Formal Methods and Tools (2009)"},{"issue":"1","key":"9_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-015-0381-2","volume":"19","author":"V Rivera","year":"2015","unstructured":"Rivera, V., Cata\u00f1o, N., Wahls, T., Rueda, C.: Code generation for Event-B. Int. J. Softw. Tools Technol. Transfer 19(1), 31\u201352 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0381-2","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Karmakar, R.: A framework for component mapping between Event-B and Python. In: Advances in Data and Information Sciences, Proceedings of RACCCS 2021, Lecture Notes in Networks and Systems. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-981-16-7952-0_13","DOI":"10.1007\/978-981-16-7952-0_13"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-24559-6_31","volume-title":"Formal Methods and Software Engineering","author":"TS Hoang","year":"2011","unstructured":"Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 456\u2013471. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24559-6_31"},{"key":"9_CR23","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-030-71187-0_10","volume-title":"Intelligent Systems Design and Applications","author":"S Guha","year":"2021","unstructured":"Guha, S., Nag, A., Karmakar, R.: Formal verification of safety-critical systems: a case-study in airbag system design. In: Abraham, A., Piuri, V., Gandhi, N., Siarry, P., Kaklauskas, A., Madureira, A. (eds.) ISDA 2020. AISC, vol. 1351, pp. 107\u2013116. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71187-0_10"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Karmakar, R.: Symbolic model checking: a comprehensive review for critical system design. In: Tiwari, S., Trivedi, M.C., Kolhe, M.L., Mishra, K., Singh, B.K. (eds.) Advances in Data and Information Sciences. LNNS, vol. 318. Springer, Singapore (2022). https:\/\/doi.org\/10.1007\/978-981-16-5689-7_62","DOI":"10.1007\/978-981-16-5689-7_62"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-91271-4_3","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"J-R Abrial","year":"2018","unstructured":"Abrial, J.-R.: On B and Event-B: principles, success and challenges. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 31\u201335. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_3"}],"container-title":["Lecture Notes in Networks and Systems","Intelligent Systems Design and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-96308-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,26]],"date-time":"2022-03-26T13:18:36Z","timestamp":1648300716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-96308-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030963071","9783030963088"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-96308-8_9","relation":{},"ISSN":["2367-3370","2367-3389"],"issn-type":[{"value":"2367-3370","type":"print"},{"value":"2367-3389","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"27 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISDA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Systems Design and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isda2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.mirlabs.net\/isda21\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}