A medida que la escala y complejidad del software crítico para la seguridad continúan creciendo, es necesario garantizar la seguridad y confiabilidad para evitar que errores menores conduzcan a desastres catastróficos. Mientras tanto, el método tradicional, como las pruebas y simulaciones por sí solas, no es suficiente para garantizar la corrección de los sistemas. Esto lleva a utilizar métodos formales para proporcionar pruebas suficientes para los sistemas. Sin embargo, diseñar un sistema crítico de seguridad de alta garantía mediante métodos formales es un desafío debido a la complejidad de los sistemas operativos. Además, el demostrador de teoremas interactivo tradicional utilizado en la verificación del sistema requiere pruebas escritas a mano, lo cual es más costoso. Por lo tanto, los esfuerzos para proporcionar un marco formal estandarizado, así como pruebas de seguridad, son notables para el desarrollo de un sistema crítico de seguridad. El propósito de este documento es proporcionar un marco de seguridad para establecer un sistema operativo altamente confiable y crítico para la seguridad basado en el estándar ARINC653, un modelo formal multinivel y estandarizado. Para verificar la corrección funcional de este modelo, proponemos un método de prueba formal basado en el contexto para programas. Para lograr este objetivo, primero modelamos 57 servicios principales de ARINC653 y definimos los requisitos de alto nivel como pre y postcondiciones. Luego, construimos un conjunto de declaraciones de especificación, un sistema de axiomas formales transformado en oraciones lógicas, y el modelo de servicio principal se transforma en una secuencia de oraciones lógicas que deben ser demostradas. Finalmente, se desarrolla un sistema de prueba formal basado en el contexto para la corrección de la especificación. Hemos verificado la corrección de los servicios principales del sistema operativo crítico para la seguridad con este sistema. La experiencia muestra que el sistema de verificación que desarrollamos puede lograr la corrección funcional de un sistema operativo completo con una carga de implementación baja, y que puede simplificar la dificultad de la verificación automatizada y aumentar el grado de automatización de la prueba.