{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T23:09:44Z","timestamp":1698966584347},"reference-count":9,"publisher":"Pleiades Publishing Ltd","issue":"4","license":[{"start":{"date-parts":[[2016,7,1]],"date-time":"2016-07-01T00:00:00Z","timestamp":1467331200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2016,7]]},"DOI":"10.1134\/s0361768816040022","type":"journal-article","created":{"date-parts":[[2016,7,22]],"date-time":"2016-07-22T06:25:59Z","timestamp":1469168759000},"page":"198-205","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Comparison of specification decomposition methods in Event-B"],"prefix":"10.1134","volume":"42","author":[{"given":"P. N.","family":"Devyanin","sequence":"first","affiliation":[]},{"given":"V. V.","family":"Kulyamin","sequence":"additional","affiliation":[]},{"given":"A. K.","family":"Petrenko","sequence":"additional","affiliation":[]},{"given":"A. V.","family":"Khoroshilov","sequence":"additional","affiliation":[]},{"given":"I. V.","family":"Shchepetkov","sequence":"additional","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2016,7,23]]},"reference":[{"key":"6306_CR1","volume-title":"Models of Security of Computer Systems: Access control and Data Flows","author":"P.N. Devyanin","year":"2013","unstructured":"Devyanin, P.N., Models of Security of Computer Systems: Access control and Data Flows, Moscow: Hot line Telecom, Moscow, 2013."},{"key":"6306_CR2","first-page":"82","volume":"7","author":"P.N. Devyanin","year":"2014","unstructured":"Devyanin, P.N., Security Conditions for Information Flows by Memory in the MROSL DP-model, Prikl. Diskr. Mat, Appendix, 2014, vol. 7, pp. 82\u201385.","journal-title":"Prikl. Diskr. Mat, Appendix"},{"key":"6306_CR3","unstructured":"Astra Linux. http:\/\/wwwastra-linuxcom"},{"key":"6306_CR4","first-page":"309","volume-title":"Proc. of the Fourth Int. Conf. on Abstract State Machines","author":"P. Devyanin","year":"2014","unstructured":"Devyanin, P., Khoroshilov, A., Kuliamin, V., et al., Formal Verification of OS Security Model with Alloy and Event-B, Proc. of the Fourth Int. Conf. on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ- 2014), Toulouse 2014, pp. 309\u2013313. https:\/\/wwwspringercom\/us\/book\/9783662436516"},{"key":"6306_CR5","volume-title":"On the Representation of the MROSL DP-model in the Formalized Event-B Notation (Rodin Platform), Konf. RusKripto-2014","author":"P.N. Devyanin","year":"2014","unstructured":"Devyanin, P.N., Kulyamin V.V., Petrenko, A.K., et al., On the Representation of the MROSL DP-model in the Formalized Event-B Notation (Rodin Platform), Konf. RusKripto-2014 (Proc. of the Conf, RusKripto- 2014), Moscow, 2014. http:\/\/wwwruscryptoru\/ resource\/ summary\/rc2014\/05_devyaninpdf"},{"key":"6306_CR6","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: Cambridge University Press, 2010."},{"issue":"6","key":"6306_CR7","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. M. Abrial","year":"2010","unstructured":"Abrial, J.-R., M. Butler, S. Hallerstede, et al., Rodin: An Open Toolset for Modelling and Reasoning in Event-B, Int. J. on Software Tools for Technol. Transfer, 2010, vol. 12, no. 6, pp. 447\u2013466.","journal-title":"Int. J. on Software Tools for Technol. Transfer"},{"key":"6306_CR8","volume-title":"Methods of Software Verification","author":"V.V. Kulyamin","year":"2008","unstructured":"Kulyamin V.V., Methods of Software Verification, Competition of Reviews on Information and Telecommunication Systems, 2008."},{"key":"6306_CR9","volume-title":"An Incremental Refinement Approach to a Development of a Flash-Based File System in Event-B","author":"K. Damchoom","year":"2010","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."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768816040022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1134\/S0361768816040022\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768816040022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T18:59:02Z","timestamp":1498330742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1134\/S0361768816040022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7]]},"references-count":9,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["6306"],"URL":"https:\/\/doi.org\/10.1134\/s0361768816040022","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7]]}}}