Método para verificar la seguridad de dispositivos controlados por computadora

Publicado el 21 Abr, 2009 por Oscar Martín en Informática

seguridad

Los ingenieros de la Universidad Carnegie Mellon de la Escuela de Ciencias de la Computación han desarrollado un nuevo método para la determinación sistemática de fallos tanto en los sistemas de prevención de colisión aéreas, como en controles de trenes de alta velocidad y otros medios, todos estos dependientes de dispositivos controlados por computadora, conocidos colectivamente como los sistemas ciber-físicos (CPS).

Este nuevo método, desarrollado por los profesores de ciencias de la computación Edmund M. Clarke y Andre Platzer, ha sido llevado recientemente a la práctica, como resultado tuvo la capacidad de detectar un error en el sistema estándar de maniobras aéreas empleado para evitar colisiones en el aire, además, también se empleó para comprobar la solidez del “Sistema de Control de Trenes Europeo”. En última instancia, este método podría utilizarse en otros sistemas ciber-físicos, tales como la cirugía robótica y la fabricación de nano-dispositivos.

Los ingenieros se basan cada vez más en las computadoras para mejorar la seguridad y la precisión de los sistemas físicos que deben interactuar con el mundo real, ya se trate de los controles de crucero adaptativo en los automóviles o en máquinas que vigilan pacientes críticos. Según comentaba el profesor Clarke; “Con sistemas cada vez más complejos, las pruebas para detectar problemas sutiles en el diseño de un sistema pueden causar disfunciones desastrosas. Nuestro método es el primero que puede probar estos complejos sistemas ciber-físicos para que funcionen como estaba previsto, o generar más contra-ejemplos de cómo pueden fallar mediante la simulación por ordenador”.

El Like Model Checking, un método pionero diseñado por el profesor Clarke, hoy día es la técnica más empleada para la detección y diagnóstico de errores complejos en el diseño de hardware y software. El nuevo método analiza la lógica que sustenta el diseño del sistema, por mucho que un matemático utilice una prueba para determinar que un teorema es correcto. El profesor Clarke comparte el A.M. Turing Award 2007, generalmente considerado en el campo de la informática el equivalente al Premio Nobel, por su papel en el desarrollo de modelos de comprobación.

Una diferencia crucial, sin embargo, es que modelo de comprobación puede examinar al máximo el estado de un discreto sistema finito, como lo sería un nuevo diseño de circuitos de un chip de computadora, esto no sería posible para un CPS que tiene que interactuar con las infinitas variables del mundo real. Incluso si las ecuaciones diferenciales que gobiernan estos sistemas se pudieran resolver (y que a menudo no pueden), por lo general sería posible utilizar los resultados para predecir el comportamiento del sistema, según nos comentaba el profesor Platzer. En vez de eso, él y Clarke han desarrollado unos algoritmos que descomponen los sistemas hasta que producen diferenciales invariantes, es decir, descripciones matemáticas de las partes del sistema que siempre siguen siendo las mismas. Estas diferenciales invariantes, a su vez, pueden ser usadas para probar la lógica global del CPS.

Según decía el profesor Platzer; “Los errores en los complejos sistemas ciber-físicos implementados en coches, aviones, chips o dispositivos médicos son caros de corregir y pueden poner en peligro la vida humana. En el transporte, el porcentaje de los costes de desarrollo invertido en el diseño y ensayo de nuevos software de control ya está muy por encima del 50 por ciento y está en constante aumento.”

La National Science Foundation (NSF) ha determinado que el diseño y la verificación de los CPS es un área clave de la investigación. El creciente uso de dispositivos robóticos, el crecimiento de redes de sensores, la propuesta de creación de una “red inteligente” para la entrega de energía eléctrica, son todos ejemplos de una creciente dependencia de los sistemas de control por computadora que están estrechamente unidas a los sistemas físicos.

Este proyecto ha sido patrocinado, en parte, por la NSF y el Consejo Alemán de Investigaciones.

Más información: Universidad de Carnegie Mellon