Innovating Works

RTC-2017-6740-7

Financiado
SOFTWARE DE FALLO CERO: Innovación de alta seguridad en el transporte pesado por...
SOFTWARE DE FALLO CERO: Innovación de alta seguridad en el transporte pesado por carretera os humanos cometen errores, En particular, los programadores cometen errores, Debe tenerse en cuenta que incluso para los proyectos de mayor envergadura y más importantes, como los software que controlan la industria aeronáutica o... os humanos cometen errores, En particular, los programadores cometen errores, Debe tenerse en cuenta que incluso para los proyectos de mayor envergadura y más importantes, como los software que controlan la industria aeronáutica o lanzamiento de cohetes de uso civil o militar, constan de errores en el producto final, Este hecho es imposible de evitar en tanto que el código es escrito y desarrollado por personas, Este hecho descrito es totalmente inaceptable y peligroso, Hay que poner de relieve que en la actualidad los programadores programan más que videojuegos, De hecho, su tarea es mucho más compleja que habilitar el vuelo de aviones, Proveen de software para mecanismos de voto electrónico, para la equipación médica, programas que discriminan entre personas que están dentro o fuera de los límites legales, y un largo etcétera, La mayor parte de estos programas no van a colapsar debido a erratas, pero aun así, pueden presentar resultados erróneos, Muy a menudo estos errores pasarán inadvertidos, lo que acarreará graves consecuencias futuras,Tenemos la posibilidad de hacerlo mejor, Hay un método por el cual podemos asegurar la creación de un software de fallo cero, El método pasa por escribir especificaciones formales, en vez de escribir directamente el software, proceso a través del cual puede extraerse directamente un software que garantiza el seguimiento de dicha especificación, La clave que marca la diferencia es que este código se extrae de pruebas matemáticas, Dichas pruebas aseguran al 100% de la corrección del código con respeto a las especificaciones formales,Este proceso constituye la vanguardia del sector, desafortunadamente, aún requiere de una gran cantidad de recursos, La verificación formal es una nueva herramienta que puede ser manejada con efectividad solamente por una minoría altamente especializada, y aun contando con un equipo de expertos requiere de una gran cantidad de tiempo, El primer paso es escribir una especificación en Inglés formalizable, junto a un código OCaml que debe realizarse acorde a la especificación, Escribir este tipo de código es enteramente distinto a cualquier proyecto de software habitual, La diferencia reside en el hecho que hay que escribir el código con especial atención para luego formalizarlo, Este primer período puede prolongarse más de un año y medio,Una vez se ha obtenido el código OCaml a través de las especificaciones el trabajo se traslada al asistente de pruebas COQ, Se formalizarán las especificaciones al lenguaje de COQ y se usará para demostrarlo y extraer un código que seguirá las especificaciones, El programa extraído por COQ será un código certificado y de error cero,El principal foco de trabajo recaerá en la formalización de la Regulación 561 sobre el transporte de mercancías y de personas por carretera en la Unión Europea, Los vehículos utilizados en este tipo de transporte se encuentran equipados con un tacógrafo, un aparato que registra el movimiento del vehículo, Los datos que se extraen del tacógrafo se leen a través de un programa no verificado llamado Police Controller, que decide si se cumple o no la ley,En otras palabras, el Police Controller toma el control del destino de numerosos conductores europeos en el seno de su código, Como cualquier otro software tradicional, comete errores, conllevando a condenas erróneas e injustas, Esto es lo hay que cambiar y vamos a cambiar, Con nuestro enfoque construiremos una alternativa formalmente verificado al Police Controller, De esta forma para cualquier lectura de tacógrafo, seremos capaces de determinar, sin fallo alguno, si se sigue o no la ley,Este proyecto no se restringe a la Unión Europea, dado que una vez poseída la estructura básica capaz de ser reutilizable, va a utilizarse en Estados Unidos, Canadá y Brasil,Para el desarrollo del proyecto se ve la necesidad de constituir un consorcio entre las dos sociedades Guretruck y Formal Vindications y la entidad pública Universidad de Barcelona, ver más
01/01/2018
GURETRUCK
227K€

Línea de financiación: concedida

El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2018-01-01
Presupuesto El presupuesto total del proyecto asciende a 227K€
Líder del proyecto
GURETRUCK Asistencia juridica nacional e internacional de la empresa de transporte, asi como la gestion de las incidencias paralelas que puedan surgir...
Sin perfil tecnológico calculado