{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:45:35Z","timestamp":1775054735930,"version":"3.50.1"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415789","type":"print"},{"value":"9783319415796","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41579-6_9","type":"book-chapter","created":{"date-parts":[[2016,6,26]],"date-time":"2016-06-26T22:44:48Z","timestamp":1466981088000},"page":"107-115","source":"Crossref","is-referenced-by-count":2,"title":["Using Refinement in Formal Development of OS Security Model"],"prefix":"10.1007","author":[{"given":"Petr N.","family":"Devyanin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey V.","family":"Khoroshilov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor V.","family":"Kuliamin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander K.","family":"Petrenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilya V.","family":"Shchepetkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,28]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR2","doi-asserted-by":"crossref","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, Cambridge (2010)"},{"issue":"6","key":"9_CR3","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"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. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1,2","key":"9_CR4","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamentae Informatica 77(1,2), 1\u201328 (2007)","journal-title":"Fundamentae Informatica"},{"key":"9_CR5","unstructured":"Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B. Ph.D. thesis, University of Southampton, School of Electronics and Computer Science (2010)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/978-3-662-43652-3_30","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"PN Devyanin","year":"2014","unstructured":"Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V.: Formal verification of OS security model with alloy and Event-B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 309\u2013313. Springer, Heidelberg (2014)"},{"key":"9_CR7","unstructured":"Devyanin, P.N.: Security models of computer systems: access control and information flows (in Russian). Hot line - Telecom (2013)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/978-3-662-43652-3_22","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"N Huynh","year":"2014","unstructured":"Huynh, N., Frappier, M., Mammar, A., Laleau, R., Desharnais, J.: Validating the RBAC ANSI 2012 standard using B. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 255\u2013270. Springer, Heidelberg (2014)"},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. CACM Commun. ACM 14, 221\u2013227 (1971)","journal-title":"CACM Commun. ACM"},{"issue":"4","key":"9_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1\u201339 (2009)","journal-title":"ACM Comput. Surv."},{"key":"9_CR11","unstructured":"Yeganefard, S., Butler, M., Rezazadeh, A.: Evaluation of a guideline by formal modelling of cruise control system in Event-B. In: NFM 2010, pp. 182\u2013191 (2010)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41579-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T13:13:20Z","timestamp":1498310000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41579-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415789","9783319415796"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41579-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}