{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T10:12:20Z","timestamp":1767262340677,"version":"3.41.0"},"reference-count":98,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T00:00:00Z","timestamp":1484092800000},"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":["Front. Comput. Sci."],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s11704-016-4226-2","type":"journal-article","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T02:02:44Z","timestamp":1484100164000},"page":"585-607","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A survey on formal specification and verification of separation kernels"],"prefix":"10.1007","volume":"11","author":[{"given":"Yongwang","family":"Zhao","sequence":"first","affiliation":[]},{"given":"Zhibin","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Dianfu","family":"Ma","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"issue":"5","key":"4226_CR1","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1067627.806586","volume":"15","author":"J Rushby","year":"1981","unstructured":"Rushby J. Design and verification of secure systems. ACM SIGOPS Operating Systems Review, 1981, 15(5): 12\u201321","journal-title":"ACM SIGOPS Operating Systems Review"},{"issue":"3-4","key":"4226_CR2","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1504\/IJES.2006.014859","volume":"2","author":"J Alves-Foss","year":"2006","unstructured":"Alves-Foss J, Oman P W, Taylor C, Harrison W S. The MILS architecture for high-assurance embedded systems. International journal of embedded systems, 2006, 2(3-4): 239\u2013247","journal-title":"International journal of embedded systems"},{"issue":"5","key":"4226_CR3","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D E Denning","year":"1976","unstructured":"Denning D E. A lattice model of secure information flow. Communications of the ACM, 1976, 19(5): 236\u2013243","journal-title":"Communications of the ACM"},{"key":"4226_CR4","volume-title":"Technical Report.","author":"T Gjertsen","year":"2008","unstructured":"Gjertsen T, Nordbotten N A. Multiple independent levels of security (MILS) \u2014 a high assurance architecture for handling information of different classification levels. Technical Report. 2008"},{"key":"4226_CR5","volume-title":"ARINC 653\u2013avionics application software standard interface","author":"ARINC Airlines Electronic Engineering Committee.","year":"2003","unstructured":"ARINC Airlines Electronic Engineering Committee. ARINC 653\u2013avionics application software standard interface. 2003"},{"key":"4226_CR6","volume-title":"Technical Report","author":"Wind river Vx Works MILS platform.","year":"2013","unstructured":"Wind river Vx Works MILS platform. Technical Report, 2013"},{"key":"4226_CR7","volume-title":"Technical Report.","author":"Green Hills Software, Inc.","year":"2005","unstructured":"Green Hills Software, Inc. Safety-critical products: Integrity-178b real-time operationg system. Technical Report. 2005"},{"key":"4226_CR8","volume-title":"Technical Report.","author":"LynuxWorks, Inc.","year":"2012","unstructured":"LynuxWorks, Inc. Lynxsecure: software security driven by an embedded hypervisor. Technical Report. 2012"},{"key":"4226_CR9","volume-title":"Technical Report.","author":"LynuxWorks, Inc.","year":"2008","unstructured":"LynuxWorks, Inc. Lynxos-se: time-and space-partitioned RTOS with open-standards apis. Technical Report. 2008"},{"key":"4226_CR10","volume-title":"Technical Report.","author":"K Robert","year":"2007","unstructured":"Robert K, Stephan W. The pikeos concept\u2014history and design. Technical Report. 2007"},{"key":"4226_CR11","volume-title":"Proceedings of the 13th Real-Time Linux Workshop.","author":"J Delange","year":"2011","unstructured":"Delange J, Lec L. Pok, an ARINC 653-compliant operating system released under the BSD license. In: Proceedings of the 13th Real-Time Linux Workshop. 2011"},{"key":"4226_CR12","volume-title":"Proceedings of the 11th Real-Time Linux Workshop.","author":"M Masmano","year":"2009","unstructured":"Masmano M, Ripoll I, Crespo A, Metge J. Xtratum: a hypervisor for safety critical embedded systems. In: Proceedings of the 11th Real-Time Linux Workshop. 2009"},{"issue":"4","key":"4226_CR13","doi-asserted-by":"crossref","first-page":"1729","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: practice and experience. ACM Computing Surveys, 2009, 41(4): 1729\u20131739","journal-title":"ACM Computing Surveys"},{"key":"4226_CR14","volume-title":"3.1 r4 edition","author":"National Security Agency.","year":"2012","unstructured":"National Security Agency. Common criteria for information technology security evaluation. 3.1 r4 edition, 2012"},{"key":"4226_CR15","volume-title":"Technical Report.","author":"National Security Agency.","year":"2007","unstructured":"National Security Agency. U.S. government protection profile for separation kernels in environments requiring high robustness. Technical Report. 2007"},{"key":"4226_CR16","volume-title":"Technical Report RTCA\/DO-178B. RTCA, Inc.","author":"Federal Aviation Authority.","year":"1992","unstructured":"Federal Aviation Authority. Software considerations in airborne systems and equipment certification. Technical Report RTCA\/DO-178B. RTCA, Inc., 1992"},{"key":"4226_CR17","volume-title":"Technical Report RTCA\/DO-178C. RTCA, Inc.","author":"Federal Aviation Authority.","year":"2011","unstructured":"Federal Aviation Authority. Software considerations in airborne systems and equipment certification. Technical Report RTCA\/DO-178C. RTCA, Inc., 2011"},{"key":"4226_CR18","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4419-1539-9_6","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"M M Wilding","year":"2010","unstructured":"Wilding M M, Greve D A, Richards R J, Hardin D S. Formal verification of partition management for the AAMP7G microprocessor. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High-Assurance Applications. Berlin: Springer, 2010, 175\u2013191"},{"key":"4226_CR19","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-04468-7_16","volume-title":"Computer Safety, Reliability, and Security","author":"C Baumann","year":"2009","unstructured":"Baumann C, Beckert B, Blasum H, Bormer T. Formal verification of a microkernel used in dependable software systems. In: Buth B, Rade G, Seyfarth T, eds. Computer Safety, Reliability, and Security. Berlin: Springer, 2009, 187\u2013200"},{"key":"4226_CR20","volume-title":"Proceedings of Doctoral Symposium on Systems Software Verification.","author":"C Baumann","year":"2009","unstructured":"Baumann C, Bormer T. Verifying the PikeOS microkernel: first results in the Verisoft XT avionics project. In: Proceedings of Doctoral Symposium on Systems Software Verification. 2009"},{"key":"4226_CR21","volume-title":"Proceedings of Embedded World Conference.","author":"C Baumann","year":"2010","unstructured":"Baumann C, Beckert B, Blasum H, Bormer T. Ingredients of operating system correctness (lessons learned in the formal verification of PikeOS). In: Proceedings of Embedded World Conference. 2010"},{"key":"4226_CR22","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/ISORCW.2011.14","volume-title":"Proceedings of the 14th IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops.","author":"C Baumann","year":"2011","unstructured":"Baumann C, Bormer T, Blasum H, Tverdyshev S. Proving memory separation in a microkernel by code level verification. In: Proceedings of the 14th IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops. 2011, 25\u201332"},{"key":"4226_CR23","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-1-4419-1539-9_10","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"R J Richards","year":"2010","unstructured":"Richards R J. Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High-Assurance Applications. Berlin: Springer, 2010, 301\u2013322"},{"key":"4226_CR24","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/1180405.1180448","volume-title":"Proceedings of the 13th ACM conference on Computer and communications security.","author":"C L Heitmeyer","year":"2006","unstructured":"Heitmeyer C L, Archer M, Leonard E I, McLean J. Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of the 13th ACM conference on Computer and communications security. 2006, 346\u2013355"},{"issue":"1","key":"4226_CR25","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"C L Heitmeyer","year":"2008","unstructured":"Heitmeyer C L, Archer M, Leonard E I, McLean J. Applying formal methods to a certifiably secure software system. IEEE Transactions on Software Engineering, 2008, 34(1): 82\u201398","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4226_CR26","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1145\/337180.337364","volume-title":"Proceedings of the 22nd international conference on Software engineering.","author":"J Penix","year":"2000","unstructured":"Penix J, Visser W, Engstrom E, Larson A, Weininger N. Verification of time partitioning in the DEOS scheduler kernel. In: Proceedings of the 22nd international conference on Software engineering. 2000, 488\u2013497"},{"issue":"2","key":"4226_CR27","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s10703-005-1490-4","volume":"26","author":"J Penix","year":"2005","unstructured":"Penix J, Visser W, Park S, Pasareanu C, Engstrom E, Larson A, Weininger N. Verifying time partitioning in the DEOS scheduling kernel. Formal Methods in System Design, 2005, 26(2): 103\u2013135","journal-title":"Formal Methods in System Design"},{"key":"4226_CR28","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1109\/ICSE.2004.1317453","volume-title":"Proceedings of the 26th International Conference on Software Engineering.","author":"V Ha","year":"2004","unstructured":"Ha V, Rangarajan M, Cofer D, Rues H, and Dutertre B. Feature-based decomposition of inductive proofs applied to real-time avionics software: an experience report. In: Proceedings of the 26th International Conference on Software Engineering. 2004, 304\u2013313"},{"issue":"3","key":"4226_CR29","first-page":"53","volume":"114","author":"W Bulkeley","year":"2011","unstructured":"Bulkeley W. Crash-proof code. MIT Technology Review, 2011, 114(3): 53\u201354","journal-title":"MIT Technology Review"},{"key":"4226_CR30","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles.","author":"G Klein","year":"2009","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles. 2009, 207\u2013220"},{"issue":"6","key":"4226_CR31","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein G, Andronick J, Elphinstone K, Heiser G, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: formal verification of an operating-system kernel. Communications of the ACM, 2010, 53(6): 107\u2013115","journal-title":"Communications of the ACM"},{"issue":"1","key":"4226_CR32","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G Klein","year":"2009","unstructured":"Klein G. Operating system verification \u2014an overview. Sadhana, 2009, 34(1): 27\u201369","journal-title":"Sadhana"},{"issue":"7","key":"4226_CR33","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/MC.1983.1654439","volume":"16","author":"S R Ames","year":"1983","unstructured":"Ames S R, Gasser M, Schell R R. Security kernel design and implementation: an introduction. Computer, 1983, 16(7): 14\u201322","journal-title":"Computer"},{"key":"4226_CR34","first-page":"12","volume-title":"MILS: architecture for high-assurance embedded computing","author":"V Mark","year":"2005","unstructured":"Mark V, William B, Ben C, Jahn L, Carol T, Gordon U. MILS: architecture for high-assurance embedded computing. CrossTalk: The Journal of Defense Software Engineering, 2005, 12\u201316"},{"key":"4226_CR35","volume-title":"Technical Report","author":"The Open Group.","year":"2003","unstructured":"The Open Group. Protection profile for partitioning kernels in environments requiring augmented high robustness. Technical Report. 2003"},{"issue":"2","key":"4226_CR36","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S1290-0958(99)80018-5","volume":"1","author":"G R Parr","year":"1999","unstructured":"Parr G R, Edwards R. Integrated modular avionics. Air & Space Europe, 1999, 1(2): 72\u201375","journal-title":"Air & Space Europe"},{"key":"4226_CR37","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/1314466.1314473","volume-title":"Proceedings of the 2007 ACM workshop on Computer security architecture.","author":"T E Levin","year":"2007","unstructured":"Levin T E, Irvine C E, Weissman C, Nguyen T D. Analysis of three multilevel security architectures. In: Proceedings of the 2007 ACM workshop on Computer security architecture. 2007, 37\u201346"},{"key":"4226_CR38","volume-title":"Technical Report.","author":"J Rushby","year":"2000","unstructured":"Rushby J. Partitioning in avionics architectures: requirements, mechanisms, and assurance. Technical Report. 2000"},{"key":"4226_CR39","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/978-3-540-75101-4_33","volume-title":"Proceedings of the 26th International Conference on Computer Safety, Reliability, and Security.","author":"B Leiner","year":"2007","unstructured":"Leiner B, Schlager M, Obermaisser R, Huber B. A comparison of partitioning operating systems for integrated systems. In: Proceedings of the 26th International Conference on Computer Safety, Reliability, and Security. 2007, 342\u2013355"},{"issue":"1","key":"4226_CR40","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/5.259426","volume":"82","author":"K Ramamritham","year":"1994","unstructured":"Ramamritham K, Stankovic J A. Scheduling algorithms and operating systems support for real-time systems. Proceedings of the IEEE, 1994, 82(1): 55\u201367","journal-title":"Proceedings of the IEEE"},{"issue":"7","key":"4226_CR41","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1145\/361011.361073","volume":"17","author":"G J Popek","year":"1974","unstructured":"Popek G J, Goldberg R P. Formal requirements for virtualizable third generation architectures. Communication of ACM, 1974, 17(7): 412\u2013421","journal-title":"Communication of ACM"},{"key":"4226_CR42","volume-title":"Proceedings of IEEE Symposium on Security and Privacy","author":"J A Goguen","year":"1982","unstructured":"Goguen J A, Meseguer J. Security policies and security models. In: Proceedings of IEEE Symposium on Security and Privacy. 1982"},{"key":"4226_CR43","first-page":"133","volume-title":"Proceedings of IEEE International Conference on Automated Software Engineering.","author":"W Martin","year":"2000","unstructured":"Martin W, White P, Taylor F S, Goldberg A. Formal construction of the mathematically analyzed separation kernel. In: Proceedings of IEEE International Conference on Automated Software Engineering. 2000, 133\u2013141"},{"issue":"3","key":"4226_CR44","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1016324624000","volume":"9","author":"WB Martin","year":"2002","unstructured":"Martin WB, White P D, Taylor F S. Creating high confidence in a separation kernel. Automated Software Engineering, 2002, 9(3): 263\u2013284","journal-title":"Automated Software Engineering"},{"key":"4226_CR45","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Proceedings of International Conference on Certified Programs and Proofs.","author":"T Murray","year":"2012","unstructured":"Murray T, Matichuk D, Brassil M, Gammie P, Klein G. Noninterference for operating system kernels. In: Proceedings of International Conference on Certified Programs and Proofs. 2012, 126\u2013142"},{"key":"4226_CR46","volume-title":"Proceedings of the ACL2 Workshop.","author":"D Greve","year":"2003","unstructured":"Greve D, Wilding M, Vaneet W M. A separation kernel formal security policy. In: Proceedings of the ACL2 Workshop. 2003"},{"key":"4226_CR47","volume-title":"Proceedings of the ACL2 Workshop.","author":"J Alves-foss","year":"2004","unstructured":"Alves-foss J, Taylor C. An analysis of the gwv security policy. In: Proceedings of the ACL2 Workshop. 2004"},{"key":"4226_CR48","volume-title":"Technical Report.","author":"Green Hills Software.","year":"2008","unstructured":"Green Hills Software. Integrity-178b separation kernel security target. Technical Report. 2008"},{"key":"4226_CR49","volume-title":"Proceedings of the ACL2 Workshop.","author":"D Greve","year":"2004","unstructured":"Greve D, Richards R, Wilding M. A summary of intrinsic partitioning verification. In: Proceedings of the ACL2 Workshop. 2004"},{"key":"4226_CR50","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-1-4419-1539-9_9","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"D Greve","year":"2010","unstructured":"Greve D. Information security modeling and analysis. In: Hardin D S, eds. Design and Verification of Microprocessor Systems for High-Assurance Applications. Berlin: Springer, 2010, 249\u2013299"},{"key":"4226_CR51","volume-title":"Technical Report, CSL Technical Note, SRI International.","author":"J Rushby","year":"2004","unstructured":"Rushby J. A separation kernel formal security policy in PVS. Technical Report, CSL Technical Note, SRI International. 2004"},{"key":"4226_CR52","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-642-20398-5_28","volume-title":"NASA Formal Methods","author":"S Tverdyshev","year":"2011","unstructured":"Tverdyshev S. Extending the GWV security policy and its modular application to a separation kernel. In: Bobaru M, Havelund K, Holzmann G J, et al. eds. NASA Formal Methods. Berlin: Springer, 2011, 391\u2013405"},{"key":"4226_CR53","volume-title":"Proceedings of the 17th Systems and Software Technology Conference.","author":"D Greve","year":"2005","unstructured":"Greve D, Wilding M, Vanfleet W M. High assurance formal security policy modeling. In: Proceedings of the 17th Systems and Software Technology Conference. 2005"},{"key":"4226_CR54","volume-title":"Technical Report, SRI International, Computer Science Laboratory.","author":"J Rushby","year":"1992","unstructured":"Rushby J. Noninterference, transitivity, and channel-control security policies. Technical Report, SRI International, Computer Science Laboratory. 1992"},{"key":"4226_CR55","first-page":"225","volume-title":"Proceedings of the 9th European Symposium on Research Computer Security.","author":"D Oheimb","year":"2004","unstructured":"Oheimb D. Information flow control revisited: noninfluence=noninterference+ nonleakage. In: Proceedings of the 9th European Symposium on Research Computer Security. 2004, 225\u2013243"},{"key":"4226_CR56","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1109\/CSFW.2001.930142","volume-title":"Proceedings of the 14th IEEE Workshop on Computer Security Foundations.","author":"H Mantel","year":"2001","unstructured":"Mantel H, Sabelfeld A. A generic approach to the security of multithreaded programs. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations. 2001, 126\u2013142"},{"key":"4226_CR57","first-page":"415","volume-title":"Proceedings of the 34th IEEE Symposium on Security and Privacy.","author":"T Murray","year":"2013","unstructured":"Murray T, Matichuk D, Brassil M, Gammie P, Bourke T, Seefried S, Lewis C, Gao X, Klein G. sel4: from general purpose to a proof of information flow enforcement. In: Proceedings of the 34th IEEE Symposium on Security and Privacy. 2013, 415\u2013429"},{"key":"4226_CR58","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-319-10506-2_17","volume-title":"Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security.","author":"A Ramirez","year":"2014","unstructured":"Ramirez A, Schmaltz J, Verbeek F, Langenstein B, Blasum H. On two models of noninterference: rushby and greve, wilding, and vanfleet. In: Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security. 2014, 246\u2013261"},{"key":"4226_CR59","volume-title":"Formal Models of Operating System Kernels","author":"I Craig","year":"2006","unstructured":"Craig I. Formal Models of Operating System Kernels. London: Springer, 2006"},{"key":"4226_CR60","volume-title":"Formal Refinement for Operating System Kernels","author":"I Craig","year":"2007","unstructured":"Craig I. Formal Refinement for Operating System Kernels. London: Springer, 2007"},{"key":"4226_CR61","first-page":"343","volume-title":"On the Construction of Programs","author":"J R Abrial","year":"1980","unstructured":"Abrial J R, Schuman S, Meyer B. Specification language. In: McKeag R M, Macnaghten A M, eds. On the Construction of Programs. Cambridge: Cambridge University Press, 1980, 343\u2013410"},{"key":"4226_CR62","first-page":"230","volume-title":"Proceedings of the 7th International colloquium conference on Theoretical aspects of computing.","author":"A Velykis","year":"2010","unstructured":"Velykis A, Freitas L. Formal modelling of separation kernel components. In: Proceedings of the 7th International colloquium conference on Theoretical aspects of computing. 2010, 230\u2013244"},{"key":"4226_CR63","volume-title":"Dissertation for the Master Degree","author":"A Velykis","year":"2009","unstructured":"Velykis A. Formal modelling of separation kernels. Dissertation for the Master Degree. York: University of York, 2009"},{"issue":"4","key":"4226_CR64","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C Jones","year":"2006","unstructured":"Jones C, O\u2019Hearn P, Woodcock J. Verified software: a grand challenge. Computer, 2006, 39(4): 93\u201395","journal-title":"Computer"},{"key":"4226_CR65","volume-title":"Upper Saddle River","author":"J Woodcock","year":"1996","unstructured":"Woodcock J, Davies J. Using Z: Specification, Refinement, and Proof. Upper Saddle River, NJ: Prentice-Hall, 1996"},{"key":"4226_CR66","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: Cambridge University press, 1996"},{"key":"4226_CR67","volume-title":"Proceedings of ESAWorkshop on Avionics Data, Control and Software Systems.","author":"P Andr\u00e9","year":"2009","unstructured":"Andr\u00e9 P. Assessing the formal development of a secure partitioning kernel with the Bmethod. In: Proceedings of ESAWorkshop on Avionics Data, Control and Software Systems. 2009"},{"key":"4226_CR68","first-page":"855","volume-title":"Proceedings of International Symposium of Formal Methods.","author":"M Leuschel","year":"2003","unstructured":"Leuschel M, Butler M. ProB: a model checker for B. In: Proceedings of International Symposium of Formal Methods. 2003, 855\u2013874"},{"key":"4226_CR69","first-page":"506","volume-title":"World Academy of Science, Engineering and Technology","author":"K Kawamorita","year":"2010","unstructured":"Kawamorita K, Kasahara R, Mochizuki Y, Noguchi K. Application of formal methods for designing a separation kernel for embedded systems. World Academy of Science, Engineering and Technology, 2010, 506\u2013514"},{"key":"4226_CR70","first-page":"281","volume-title":"Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering.","author":"Y W Zhao","year":"2015","unstructured":"Zhao Y W, Yang Z B, Sanan D, Liu Y. Event-based formalization of safety-critical operating system standards: an experience report on ARINC 653 using Event-B. In: Proceedings of the 26th IEEE International Symposium on Software Reliability Engineering. 2015, 281\u2013292"},{"issue":"1-2","key":"4226_CR71","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. Fundamenta Informaticae, 2007, 77(1-2): 1\u201328","journal-title":"Fundamenta Informaticae"},{"key":"4226_CR72","volume-title":"Archive of Formal Proofs","author":"F Verbeek","year":"2014","unstructured":"Verbeek F, Schmaltz J, Tverdyshev S, Havle O, Blasum H, Langenstein B, Stephan W, Feliachi A, Nemouchi Y, Wotff B. Formal specification of a generic separation kernel. Archive of Formal Proofs, 2014"},{"key":"4226_CR73","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-319-17524-9_26","volume-title":"NASA Formal Methods","author":"F Verbeek","year":"2015","unstructured":"Verbeek F, Havle O, Schmaltz J, Tverdyshev S, Blasum H, Langenstein B, Stephan W, Wolff B, Nemouchi Y. Formal API specification of the PikeOS separation kernel. In: Havelund K, Holzmann G, Joshi R, eds. NASA Formal Methods. Springer, 2015, 375\u2013389"},{"key":"4226_CR74","volume-title":"Proceedings of the 1st International Workshop on Microkernels for Embedded Systems.","author":"R Kaiser","year":"2007","unstructured":"Kaiser R, Wagner S. Evolution of the pikeos microkernel. In: Proceedings of the 1st International Workshop on Microkernels for Embedded Systems. 2007"},{"key":"4226_CR75","volume-title":"Proceedings of Embedded World Conference.","author":"C Baumann","year":"2009","unstructured":"Baumann C, Beckert B, Blasum H, Bormer T. Better avionics software reliability by code verification? A glance at code verification methodology in the Verisoft XT project. In: Proceedings of Embedded World Conference. 2009"},{"key":"4226_CR76","first-page":"223","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer & Communications Security.","author":"M Dam","year":"2013","unstructured":"Dam M, Guanciale R, Khakpour N, Nemati H, Schwarz O. Formal verification of information flow security for a simple arm-based separation kernel. In: Proceedings of the ACM SIGSAC Conference on Computer & Communications Security. 2013, 223\u2013234"},{"key":"4226_CR77","doi-asserted-by":"crossref","first-page":"791","DOI":"10.1007\/978-3-662-49674-9_50","volume-title":"Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Y Zhao","year":"2016","unstructured":"Zhao Y, Sanan D, Zhang F, Liu Y. Reasoning about information flow security of separation kernels with channel-based communication. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2016, 791\u2013810"},{"key":"4226_CR78","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/1435458.1435461","volume-title":"Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems.","author":"G Heiser","year":"2008","unstructured":"Heiser G. The role of virtualization in embedded systems. In: Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems. 2008, 11\u201316"},{"key":"4226_CR79","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1145\/2420950.2421011","volume-title":"Proceedings of the 28th Annual Computer Security Applications Conference.","author":"J McDermott","year":"2012","unstructured":"McDermott J, Montrose B, Li M, Kirby J, Kang M. Separation virtual machine monitors. In: Proceedings of the 28th Annual Computer Security Applications Conference. 2012, 419\u2013428"},{"key":"4226_CR80","first-page":"67","volume-title":"Proceedings of the 8th European Dependable Computing Conference (EDCC).","author":"A Crespo","year":"2010","unstructured":"Crespo A, Ripoll I, Masmano M. Partitioned embedded architecture based on hypervisor: the XtratuM approach. In: Proceedings of the 8th European Dependable Computing Conference (EDCC). 2010, 67\u201372"},{"key":"4226_CR81","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1109\/SP.2010.29","volume-title":"Proceedings of the 2010 IEEE Symposium on Security and Privacy.","author":"J Franklin","year":"2010","unstructured":"Franklin J, Chaki S, Datta A, Seshadri A. Scalable parametric verification of secure systems: how to verify reference monitors without worrying about data structure size. In: Proceedings of the 2010 IEEE Symposium on Security and Privacy. 2010, 365\u2013379"},{"issue":"1","key":"4226_CR82","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-642-28641-4_4","volume":"7215","author":"J Franklin","year":"2012","unstructured":"Franklin J, Chaki S, Datta A, McCune J M, Vasudevan A. Parametric verification of address space separation. Lecture Notes in Computer Science. 2012, 7215(1): 51\u201368","journal-title":"Lecture Notes in Computer Science."},{"key":"4226_CR83","first-page":"231","volume-title":"Proceedings of International Symposium on Formal Methods.","author":"G Barthe","year":"2011","unstructured":"Barthe G, Betarte G, Campo J D, Luna C. Formally verifying isolation and availability in an idealized model of virtualization. In: Proceedings of International Symposium on Formal Methods. 2011, 231\u2013245"},{"issue":"1","key":"4226_CR84","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.istr.2008.01.001","volume":"13","author":"J McDermott","year":"2008","unstructured":"McDermott J, Kirby J, Montrose B, Johnson T, Kang M. Reengineering Xen internals for higher-assurance security. Information Security Technical Report, 2008, 13(1): 17\u201324","journal-title":"Information Security Technical Report"},{"key":"4226_CR85","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1456396.1456401","volume-title":"Proceedings of the 6th ACM workshop on Formal methods in security engineering.","author":"J McDermott","year":"2008","unstructured":"McDermott J, Freitas L. A formal security policy for Xenon. In: Proceedings of the 6th ACM workshop on Formal methods in security engineering. 2008, 43\u201352"},{"key":"4226_CR86","first-page":"33","volume-title":"Proceedings of the 3rd European Symposium on Research in Computer Security.","author":"A Roscoe","year":"1994","unstructured":"Roscoe A, Woodcock J, Wulf L. Non-interference through determinism. In: Proceedings of the 3rd European Symposium on Research in Computer Security. 1994, 33\u201353"},{"key":"4226_CR87","first-page":"118","volume-title":"Proceedings of the 16th Ada-Europe International Conference on Reliable Software Technologies.","author":"L Carnevali","year":"2011","unstructured":"Carnevali L, Lipari G, Pinzuti A, Vicario E. A formal approach to design and verification of two-level hierarchical scheduling systems. In: Proceedings of the 16th Ada-Europe International Conference on Reliable Software Technologies. 2011, 118\u2013131"},{"issue":"5","key":"4226_CR88","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1109\/TSE.2012.54","volume":"39","author":"L Carnevali","year":"2013","unstructured":"Carnevali L, Pinzuti A, Vicario E. Compositional verification for hierarchical scheduling of real-time systems. IEEE Transactions on Software Engineering, 2013, 39(5): 638\u2013657","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4226_CR89","first-page":"172","volume-title":"Proceedings of the 23rd Euromicro Conference on Real-Time Systems (ECRTS).","author":"M Asberg","year":"2011","unstructured":"Asberg M, Pettersson P, Nolte T. Modelling, verification and synthesis of two-tier hierarchical fixed-priority preemptive scheduling. In: Proceedings of the 23rd Euromicro Conference on Real-Time Systems (ECRTS). 2011, 172\u2013181"},{"issue":"8","key":"4226_CR90","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1016\/j.ic.2007.01.009","volume":"205","author":"E Fersman","year":"2007","unstructured":"Fersman E, Krcal P, Pettersson P, Wang Y. Task automata: schedulability, decidability and undecidability. Information and Computation, 2007, 205(8): 1149\u20131172","journal-title":"Information and Computation"},{"issue":"3","key":"4226_CR91","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1145\/1315607.1315593","volume":"27","author":"F Singhoff","year":"2007","unstructured":"Singhoff F, Plantec A. AADL modeling and analysis of hierarchical schedulers. ACM SIGAda Ada Letters, 2007, 27(3): 41\u201350","journal-title":"ACM SIGAda Ada Letters"},{"key":"4226_CR92","volume-title":"Proceedings of the 9th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing.","author":"A Zerzelidis","year":"2006","unstructured":"Zerzelidis A, Wellings A. Getting more flexible scheduling in the RTSJ. In: Proceedings of the 9th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. 2006"},{"issue":"1","key":"4226_CR93","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1145\/1814539.1814542","volume":"10","author":"A Zerzelidis","year":"2010","unstructured":"Zerzelidis A, Wellings A. A framework for flexible scheduling in the RTSJ. ACM Transactions on Embedded Computing Systems, 2010, 10(1): 501\u2013512","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"4226_CR94","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/1167999.1168005","volume-title":"Proceedings of the 4th International Workshop on Java Technologies for Realtime and Embedded Systems","author":"A Zerzelidis","year":"2006","unstructured":"Zerzelidis A, Wellings A. Model-based verification of a framework for flexible scheduling in the real-time specification for Java. In: Proceedings of the 4th International Workshop on Java Technologies for Realtime and Embedded Systems, 2006, 20\u201329"},{"key":"4226_CR95","doi-asserted-by":"crossref","first-page":"815","DOI":"10.1007\/978-1-4419-5906-5_865","volume-title":"Encyclopedia of Cryptography and Security","author":"J Alves-Foss","year":"2011","unstructured":"Alves-Foss J. Multiple independent levels of security. In: Van Tilborg H C A, Jajodia S, eds. Encyclopedia of Cryptography and Security. Springer US, 2011, 815\u2013818"},{"issue":"6","key":"4226_CR96","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M Clarkson","year":"2010","unstructured":"Clarkson M, Schneider F. Hyperproperties. Journal of Computer Security, 2010, 18(6): 1157\u20131210","journal-title":"Journal of Computer Security"},{"key":"4226_CR97","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Proceedings of International Conference on Principles of Security and Trust.","author":"M R Clarkson","year":"2014","unstructured":"Clarkson M R, Finkbeiner B, Koleini M, Micinski K K, Rabe M N, S\u00e1nchez C. Temporal logics for hyperproperties. In: Proceedings of International Conference on Principles of Security and Trust. 2014, 265\u2013284"},{"key":"4226_CR98","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1145\/1134285.1134406","volume-title":"Proceedings of the 28th International Conference on Software Engineering.","author":"J R Abrial","year":"2006","unstructured":"Abrial J R. Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering. 2006, 761\u2013768"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-016-4226-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-4226-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-016-4226-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T07:07:38Z","timestamp":1749884858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-016-4226-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,11]]},"references-count":98,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["4226"],"URL":"https:\/\/doi.org\/10.1007\/s11704-016-4226-2","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"type":"print","value":"2095-2228"},{"type":"electronic","value":"2095-2236"}],"subject":[],"published":{"date-parts":[[2017,1,11]]}}}