{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T04:43:24Z","timestamp":1775018604268,"version":"3.50.1"},"reference-count":16,"publisher":"Pleiades Publishing Ltd","issue":"7","license":[{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,1]],"date-time":"2023-12-01T00:00:00Z","timestamp":1701388800000},"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,12]]},"DOI":"10.1134\/s0361768823070034","type":"journal-article","created":{"date-parts":[[2023,12,7]],"date-time":"2023-12-07T14:02:14Z","timestamp":1701957734000},"page":"559-565","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Runtime Verification of Operating Systems Based on Abstract Models"],"prefix":"10.1134","volume":"49","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9916-056X","authenticated-orcid":false,"given":"D. V.","family":"Efremov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2461-9986","authenticated-orcid":false,"given":"V. V.","family":"Kopach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9303-3132","authenticated-orcid":false,"given":"E. V.","family":"Kornykhin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3439-9534","authenticated-orcid":false,"given":"V. V.","family":"Kuliamin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7411-3831","authenticated-orcid":false,"given":"A. K.","family":"Petrenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6512-4632","authenticated-orcid":false,"given":"A. V.","family":"Khoroshilov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5794-004X","authenticated-orcid":false,"given":"I. V.","family":"Shchepetkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"137","published-online":{"date-parts":[[2023,12,7]]},"reference":[{"key":"3770_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 University Press, 2010."},{"key":"3770_CR2","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-41579-6_9","volume":"9609","author":"P.N. Devyanin","year":"2016","unstructured":"Devyanin, P.N., Khoroshilov, A.V., et al., Using refinement in formal development of OS security model, Lect. Notes Comput. Sci., 2016, vol. 9609, pp. 107\u2013115.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3770_CR3","doi-asserted-by":"crossref","unstructured":"Kuliamin, V., Khoroshilov, A., and Medveded, D., Formal modeling of multi-level security and integrity control implemented with SELinux, Proc. Int. Conf. Actual Problems of Systems and Software Engineering (APSSE), 2019, pp. 131\u2013136.","DOI":"10.1109\/APSSE47353.2019.00024"},{"key":"3770_CR4","doi-asserted-by":"publisher","unstructured":"Petrenko, A.K., Efremov, D.V., et al., Monitoring and testing based on multi-level program specifications, Tr. Inst. Sist. Program. Ross. Akad. Nauk 2020, vol. 32, no. 6, pp. 7\u201318. https:\/\/doi.org\/10.15514\/ISPRAS-2020-32(6)-1","DOI":"10.15514\/ISPRAS-2020-32(6)-1"},{"key":"3770_CR5","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., et al., Rodin: An open toolset for modelling and reasoning in Event-B, Int. J. Software Tools Technol. Transfer, 2010, vol. 12, no. 6, pp. 447\u2013466.","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"3770_CR6","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N. Wirth","year":"1971","unstructured":"Wirth, N., Program development by stepwise refinement, Commun. ACM, 1971, vol. 14, no. 4, pp. 221\u2013227.","journal-title":"Commun. ACM"},{"key":"3770_CR7","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume":"2805","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M. and Butler, M., ProB: A model checker for B, Lect. Notes Comput. Sci., 2003, vol. 2805, pp.\u00a0855\u2013874.","journal-title":"Lect. Notes Comput. Sci."},{"key":"3770_CR8","doi-asserted-by":"crossref","unstructured":"Khoroshilov, A., Kuliamin, V., et al., A state-based refinement technique for Event-B, Proc. Ivannikov Memorial Workshop (IVMEM), 2020, pp. 49\u201354.","DOI":"10.1109\/IVMEM51402.2020.00015"},{"key":"3770_CR9","unstructured":"Kroah-Hartman, G., LSM: Add all of the new security\/* files for basic task control. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/tglx\/history.git\/commit?id=2b15fe6334aebd7d3340f8b826acb79b138afa74. Accessed January 15, 2022."},{"key":"3770_CR10","unstructured":"Edge, J., Progress in security module stacking. \nhttps:\/\/lwn.net\/Articles\/635771. Accessed January 15, 2022."},{"key":"3770_CR11","unstructured":"Edge, J., LSM stacking and the future. \nhttps:\/\/lwn.net\/Articles\/804906. Accessed January 15, 2022."},{"key":"3770_CR12","unstructured":"Linux Integrity Subsystem. http:\/\/linux-ima.sourceforge.net. Accessed January 15, 2022."},{"key":"3770_CR13","doi-asserted-by":"crossref","unstructured":"Edwards, A., Jaeger, T., and Zhang, X., Runtime verification of authorization hook placement for the Linux security modules framework, Proc. 9th ACM Conf. Computer and Communications Security, 2002, pp. 225\u2013234.","DOI":"10.1145\/586110.586141"},{"key":"3770_CR14","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/996943.996944","volume":"7","author":"T. Jaeger","year":"2004","unstructured":"Jaeger, T., Edwards, A., and Zhang, X., Consistency analysis of authorization hook placement in the Linux security modules framework, ACM Trans. Inf. Syst. Secur., 2004, vol. 7, no. 2, pp. 175\u2013205.","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"3770_CR15","doi-asserted-by":"crossref","unstructured":"Rubanov, V.V. and Shatokhin, E.A., Runtime verification of Linux kernel modules based on call interception, Proc. 4th IEEE Int. Conf. Software Testing, Verification, and Validation, 2011, pp. 180\u2013189.","DOI":"10.1109\/ICST.2011.20"},{"key":"3770_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-030-30446-1_17","volume":"11724","author":"D.B. de Oliveira","year":"2019","unstructured":"de Oliveira, D.B., Cucinotta, T., and de Oliveira, R.S., Efficient formal verification for the Linux kernel, Lect. Notes Comput. Sci., 2019, vol. 11724, pp. 315\u2013332.","journal-title":"Lect. Notes Comput. Sci."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823070034.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768823070034","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823070034.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:54:11Z","timestamp":1775012051000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768823070034"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12]]},"references-count":16,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["3770"],"URL":"https:\/\/doi.org\/10.1134\/s0361768823070034","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12]]},"assertion":[{"value":"10 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 January 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 December 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}