•  I
• a · A  I
• Accesibilidad  I
• Mapa web  I
• Buscar  I
• Directorio

• ::  Iniciar sesión :: 

La ausencia de errores es la gran quimera de la industria del software. Si tenemos en cuenta el peso de la informática en la sociedad actual, en todos los ámbitos, desde las apps que descargamos en nuestros móviles hasta sectores críticos como el control del tráfico o las transacciones bancarias, garantizar la ausencia de errores de los programas informáticos que hay detrás de ellos es cada vez más necesario.

Con este objetivo, un equipo de la Universitat Politècnica de València (UPV), perteneciente al Instituto Valenciano de Inteligencia Artificial (VRAIN), participa en EuroProofNet, una red de investigación europea sobre pruebas digitales cuyo objetivo es contribuir a lograr el software libre de errores. Su puesta en marcha se enmarca dentro de una acción COST (European Cooperation in Science and Technology) sobre pruebas formales de software que persigue poner a Europa al frente del liderazgo de la verificación formal.

Tal y como destaca Alicia Villanueva, investigadora del Instituto VRAIN de la UPV, hoy en día existe software muy seguro porque pasa por un análisis y verificación formal muy exigente. Estas pruebas son claves, porque el menor de los fallos puede provocar grandes desastres humanos, materiales o económicos. Y lo son a todos los niveles.

“Por ejemplo, a veces no somos conscientes de la importancia de que las apps de nuestros móviles sean verificadas. Muchas de ellas gestionan nuestros datos, nuestras cuentas, por lo que cualquier vulnerabilidad puede afectar tanto a los usuarios como a las propias empresas desarrolladoras. Por eso es importante intentar avanzar no solo en el desarrollo de las propias técnicas sino también en hacer las herramientas más accesibles. Hoy en día no solo son críticos los sistemas de control aeronáuticos, ferroviarios, etc. que tienen presupuestos millonarios y para los que ya hemos aceptado la necesidad de garantizar su corrección. Haciendo más accesibles las herramientas de verificación formal podremos ayudar a mejorar la seguridad y calidad de cualquier sistema software”, apunta Villanueva.

La UPV, al frente de la investigación en verificación de programas

La red cuenta con más de 200 investigadores e investigadoras, de 30 países, tanto de la Unión Europea como de fuera de ella, e incluye seis grupos de trabajo, cada uno de ellos especializado en un área concreta. El equipo de VRAIN-UPV lidera el grupo que trabaja en la verificación de programas.

“En este grupo, lo que tratamos de mejorar son las técnicas de verificación formal que a su vez hacen uso de los sistemas de prueba formales. La principal característica de la verificación formal es que es capaz de garantizar que una propiedad se cumple para cualquier posible ejecución, contribuyendo así a la seguridad del software”, explica Alicia Villanueva.

Aunque hoy en día existen multitud de herramientas de verificación eficaces, muchas veces se especializan en resolver un tipo de problema concreto. En este contexto EuroProofNet tiene dos grandes objetivos: por un lado, mejorar las interoperabilidad y usabilidad de los sistemas de prueba formales, para así contribuir al avance de las herramientas de verificación que hacen uso de ellos y, por otro, mejorar la interoperabilidad entre sistemas de verificación para aprovechar lo mejor de cada técnica. “Todo ello contribuirá a garantizar la seguridad de los programas informáticos”, remarca Alicia Villanueva.

Además de los objetivos puramente científicos, EuroProofNet pretende construir una red de investigadores que fomente la colaboración y ayude a avanzar en este sentido. La red desarrollará sus actividades hasta octubre de 2025.