{"id":104790,"date":"2022-08-07T21:36:50","date_gmt":"2022-08-07T19:36:51","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra"},"modified":"2022-08-07T21:36:50","modified_gmt":"2022-08-07T19:36:51","slug":"dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","status":"publish","type":"post","link":"https:\/\/prohoster.info\/es\/blog\/news\/dlya-linux-predlozhen-mehanizm-verifikaczii-korrektnosti-raboty-yadra","title":{"rendered":"Se propone un mecanismo para la verificaci\u00f3n de la correcci\u00f3n del n\u00facleo en Linux","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Para incluir en el n\u00facleo de Linux 5.20 (posiblemente, la rama recibir\u00e1 el n\u00famero 6.0) se ha propuesto un conjunto de parches con la implementaci\u00f3n del mecanismo RV (Verificaci\u00f3n en Tiempo de Ejecuci\u00f3n), que proporciona herramientas para verificar la correcci\u00f3n del funcionamiento en sistemas de alta confiabilidad, garantizando la ausencia de fallos. La verificaci\u00f3n se realiza en tiempo de ejecuci\u00f3n mediante la vinculaci\u00f3n de controladores a puntos de seguimiento, que comparan el flujo de ejecuci\u00f3n real con un modelo de aut\u00f3mata determinista previamente definido, que determina el comportamiento esperado del sistema. <\/p>\n
La informaci\u00f3n de los puntos de traza transforma el modelo de un estado a otro, y si el nuevo estado no cumple con los par\u00e1metros del modelo, se genera una advertencia o el n\u00facleo se traduce al estado «panic» (se supone que sistemas de alta confiabilidad detectar\u00e1n tales situaciones y reaccionar\u00e1n ante ellas). El modelo de aut\u00f3mata, que define las transiciones de un estado a otro, se exporta al formato «dot» (graphviz), despu\u00e9s se traduce mediante la herramienta dot2c a la representaci\u00f3n en lenguaje C, que se carga en forma de un m\u00f3dulo del n\u00facleo, el cual supervisa las desviaciones de la ejecuci\u00f3n respecto al modelo predefinido.
<\/center> <\/p>\n
La comparaci\u00f3n con el modelo durante la ejecuci\u00f3n se posiciona como un m\u00e9todo m\u00e1s ligero y f\u00e1cil de implementar en la pr\u00e1ctica para confirmar la correcci\u00f3n de la ejecuci\u00f3n en sistemas cr\u00edticos, complementando los m\u00e9todos cl\u00e1sicos de verificaci\u00f3n de confiabilidad, como la verificaci\u00f3n del modelo y las pruebas matem\u00e1ticas de conformidad del c\u00f3digo con las especificaciones establecidas en un lenguaje formal. Entre las ventajas del RV se menciona la posibilidad de asegurar una verificaci\u00f3n rigurosa sin necesidad de implementar todo el sistema en un lenguaje de modelado, as\u00ed como una respuesta flexible ante eventos imprevistos, por ejemplo, para bloquear la propagaci\u00f3n adicional de fallos en sistemas cr\u00edticos. \n Fuente: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"
![\"Se](\"\/wp-content\/uploads\/2022\/08\/56f02964c804a17b5cf5d811b2777368.jpg\")
<\/center> <\/p>\n