{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T04:43:17Z","timestamp":1775018597060,"version":"3.50.1"},"reference-count":33,"publisher":"Pleiades Publishing Ltd","issue":"5","license":[{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"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":["Program Comput Soft"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1134\/s0361768823050079","type":"journal-article","created":{"date-parts":[[2023,10,9]],"date-time":"2023-10-09T04:55:24Z","timestamp":1696827324000},"page":"470-483","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automata-Based Software Engineering with Event-B"],"prefix":"10.1134","volume":"49","author":[{"given":"V. I.","family":"Shelekhov","sequence":"first","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2023,10,9]]},"reference":[{"key":"3762_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Modeling in Event-B: System and Software Engineering, Cambridge: Cambridge Univ. Press, 2010."},{"key":"3762_CR2","volume-title":"Rodin User\u2019s Handbook, Version 2.8","year":"2014","unstructured":"Rodin User\u2019s Handbook, Version 2.8, Ed. by Jastram, M., 2014."},{"key":"3762_CR3","series-title":"The first twenty-five years of industrial use of the B-Method","volume-title":"Formal Methods for Industrial Critical Systems","author":"M.J. Butler","year":"2020","unstructured":"Butler, M.J., K\u00f6rner, P., Krings, S., Lecomte, T., Leuschel, M., Mejia, L.-F., and Voisin, L., The first twenty-five years of industrial use of the B-Method, in Formal Methods for Industrial Critical Systems \n               (FMICS), 2020, pp. 189\u2013209."},{"key":"3762_CR4","unstructured":"Kharnaukhov, N., Perchine, D., and Shelekhov, V., The Predicate Programming Language P, Novosibirsk: Inst. Sistem Informatiki, Sib. Otd. Russ, Akad. Nauk, 2018 [in Russian]. \nhttp:\/\/persons.iis.nsk.su\/files\/persons\/pages\/plang14.pdf . Accessed February 9, 2022."},{"key":"3762_CR5","unstructured":"Shelekhov, V.I., Automata-based software engineering: The language and development methods. Program. Ingeneriya, 2014, No. 4, pp. 3\u201315. \nhttp:\/\/persons.iis.nsk.su\/files\/persons\/pages\/automatProg.pdf. Accessed February 9, 2022."},{"key":"3762_CR6","doi-asserted-by":"crossref","unstructured":"Tumurov, E.G. and Shelekhov, V. I., Applying automata-based software engineering for the elevator control program, Program. Ingeneriya, 2017, vol. 8, no. 4, pp.\u00a099\u2013111. http:\/\/persons.iis.nsk.su\/files\/persons\/pages\/lift1.pdf. Accessed February 9, 2022.","DOI":"10.17587\/prin.8.99-111"},{"key":"3762_CR7","unstructured":"Shelekhov, V.I., Automata-based programming on the basis of requirement specifications, System Informatics, 2015, no. 1, pp. 1\u201329. \nhttp:\/\/persons.iis.nsk.su\/files\/persons\/pages\/req_tech.pdf. Accessed February 9, 2022."},{"key":"3762_CR8","unstructured":"Shelekhov, V.I., Automata-based program optimization by applying requirement transformations, Program. Inzheneriya, 2015, no. 11, pp. 3\u201313. \nhttp:\/\/persons.iis.nsk.su\/files\/persons\/pages\/req_k.pdf. Accessed February 9, 2022."},{"key":"3762_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A. R. Hoare","year":"1969","unstructured":"Hoare, C.A. R., An axiomatic basis for computer programming, Commun. ACM, 1969, vol. 12, no. 10, pp.576\u2013585.","journal-title":"Commun. ACM"},{"key":"3762_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W., Assigning meanings to programs. Proc. of the Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, AMS, 1967. pp. 19\u201332.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"3762_CR11","doi-asserted-by":"crossref","unstructured":"Shelekhov, V.I., Program classification in software engineering, Program. Ingeneriya, 2016, vol. 7, no. 12, pp.\u00a0531\u2013538. \nhttps:\/\/persons.iis.nsk.su\/files\/persons\/pages\/prog.pdf. Accessed February 9, 2022.","DOI":"10.17587\/prin.7.531-538"},{"key":"3762_CR12","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/942572.807045","volume":"9","author":"B. Liskov","year":"1974","unstructured":"Liskov, B. and Zilles, S., Programming with abstract data types, Proc. of the ACM SIGPLAN Symposium on Very High Level Languages, \n               SIGPLAN Notices, 1974, vol. 9, pp. 50\u201359.","journal-title":"SIGPLAN Notices"},{"key":"3762_CR13","unstructured":"Systems and software engineering \u2014 Life cycle processes \u2014 Requirements engineering. ISO\/IEC\/ IEEE 29148, 2011."},{"key":"3762_CR14","unstructured":"Shelekhov, V.I., Development of a program for building a suffix tree in the predicate software engineering, Preprint of Institute of Informatics Systems, Novosibirsk, 2004, no. 115, 52p."},{"key":"3762_CR15","unstructured":"Shelekhov, V., Development and verification of the heapsort algorithms using the predicate programming technology, Preprint of Institute of Informatics Systems, Novosibirsk, 2012, no. 164, 30 p."},{"key":"3762_CR16","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume":"607","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., and Shankar, N., PVS: Specification and Verification System. CADE-11: Automated Deduction. Lect. Notes Comput. Sci., 1992, vol. 607, p. 748\u2013752.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3762_CR17","unstructured":"Why 3. Where Programs Meet Provers, available at: http:\/\/why3.lri.fr. Accessed February 9, 2022."},{"key":"3762_CR18","unstructured":"The Coq Proof Assistant, available at http:\/\/coq.inria.fr. Accessed February 9, 2022."},{"key":"3762_CR19","doi-asserted-by":"crossref","unstructured":"Shelekhov, V.I., Comparison of automata-based engineering method and Event-B modeling metho, Sist. Inform., 2021, no. 18, pp. 53\u201384. \nhttps:\/\/persons.iis.nsk.su\/files\/persons\/pages\/bridge.pdf. Accessed February 9, 2022.","DOI":"10.31144\/si.2307-6410.2021.n18.p53-84"},{"key":"3762_CR20","unstructured":"Shalyto, A.A., SWITCH-technology: Algorithmic and Programming Methods in Solution of Logic Control Problems, St. Petersburg: Nauka, 1998 [in Russian]. http:\/\/is.ifmo.ru\/books\/switch\/1. Accessed February 9, 2022."},{"key":"3762_CR21","unstructured":"Specification and description language (SDL). ITU-T Recommendation Z.100 (03\/93). \nhttp:\/\/www.itu.int\/ITU-T\/studygroups\/com17\/languages\/Z100.pdf. Accessed February 9, 2022."},{"key":"3762_CR22","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L. Lamport","year":"2021","unstructured":"Lamport, L., Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2021."},{"key":"3762_CR23","unstructured":"Parondzanov, V.D., DRAKON Language: Short Description, Moscow: 2009 [in Russian]. http:\/\/drakon.su\/_media\/biblioteka\/drakondescription.pdf. Accessed February 9, 2022."},{"key":"3762_CR24","volume-title":"Automata-Based Programming","author":"N.I. Polykarpova","year":"2020","unstructured":"Polykarpova, N.I. and Shalyto, A.A., Automata-Based Programming, 2nd ed., St. Petersburg: Piter, 2020 [in Russian]."},{"key":"3762_CR25","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Dghaym, D., Snook, C., and Butler, M., A composition mechanism for refinement-based methods, 22nd Int. Conference on Engineering of Complex Computer Systems (ICECCS), 2017, pp. 100\u2013109.","DOI":"10.1109\/ICECCS.2017.27"},{"key":"3762_CR26","volume-title":"The B-book\u2014Assigning Programs to Meanings","author":"J.-R. Abrial","year":"2005","unstructured":"Abrial, J.-R., The B-book\u2014Assigning Programs to Meanings, Cambridge Univ. Press, 2005."},{"key":"3762_CR27","volume-title":"Communication and Concurrency. International Series in Computer Science","author":"R. Milner","year":"1989","unstructured":"Milner, R., Communication and Concurrency. International Series in Computer Science, Prentice Hall, 1989."},{"key":"3762_CR28","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall Int., 1985."},{"key":"3762_CR29","doi-asserted-by":"crossref","unstructured":"Larson, J., Erlang for concurrent programming, ACM Queue, 2008, No. 5, pp. 18\u201323.","DOI":"10.1145\/1454456.1454463"},{"key":"3762_CR30","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-030-61470-6_16","volume":"12477","author":"R.D. Nicola","year":"2020","unstructured":"Nicola, R.D., Duong, T., and Inverso, O., Verifying AbC specifications via emulation. leveraging applications of formal methods, verification and validation: Engineering principles, ISoLA, Part II, Lect. Notes Comput. Sci., 2020, vol. 12477, pp. 261\u2013279.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3762_CR31","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_22","volume-title":"Verifying asynchronous event-driven programs using partial abstract transformers.","author":"P. Liu","year":"2019","unstructured":"Liu, P., Wahl, T., and Lal, A., Verifying asynchronous event-driven programs using partial abstract transformers. Computer Aided Verification, Lect. Notes Comput. Sci., 2019, vol. 11562, pp. 386\u2013404."},{"key":"3762_CR32","series-title":"Lect. Notes Comput. Sci.","volume-title":"Programming safe robotics systems: Challenges and advances.","author":"A. Desai","year":"2018","unstructured":"Desai, A., Qadeer, S., and Seshia, S.A., Programming safe robotics systems: Challenges and advances. Leveraging Applications of Formal Methods, Verification and Validation. Verification, Lect. Notes Comput. Sci., 2018, vol. 11245, pp. 103\u2013119."},{"key":"3762_CR33","volume-title":"Event-Driven Programming: Introduction, Tutorial, History","author":"S. Ferg","year":"2006","unstructured":"Ferg, S., Event-Driven Programming: Introduction, Tutorial, History, SourceForge, 2006."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823050079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768823050079","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823050079.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:54:06Z","timestamp":1775012046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768823050079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["3762"],"URL":"https:\/\/doi.org\/10.1134\/s0361768823050079","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10]]},"assertion":[{"value":"9 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 February 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 March 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 October 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}