{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:38:54Z","timestamp":1775054334555,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662436516","type":"print"},{"value":"9783662436523","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_30","type":"book-chapter","created":{"date-parts":[[2014,5,28]],"date-time":"2014-05-28T22:22:12Z","timestamp":1401315732000},"page":"309-313","source":"Crossref","is-referenced-by-count":12,"title":["Formal Verification of OS Security Model with Alloy and Event-B"],"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","reference":[{"key":"30_CR1","unstructured":"Devyanin, P.N.: The models of security of computer systems: access control and information flows. Hot line - Telecom, Moscow (2013) (in Russian)"},{"key":"30_CR2","volume-title":"Computer security: art and science","author":"M. Bishop","year":"2002","unstructured":"Bishop, M.: Computer security: art and science. Pearson Education Inc., Boston (2002)"},{"key":"30_CR3","unstructured":"Wright, C., Cowan, C., Smalley, S., Morris, J., Kroah-Hartman, G.: Linux Security Modules: General Security Support for the Linux Kernel. In: Proc. of the 11th USENIX Security Symposium, pp. 17\u201331 (2002)"},{"key":"30_CR4","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"30_CR6","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., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer\u00a012(6), 447\u2013466 (2010)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"30_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd Your Herd of Provers. In: Proc. of Boogie\u00a02011: 1st Intl Workshop on Intermediate Verification Languages, pp. 53\u201364 (2011)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T19:24:47Z","timestamp":1558898687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}