Un producto para la Uni\u00f3n Europea, Estados Unidos, Brasil y Canad\u00e1<\/strong><\/p>\n La primera fase del proyecto es la creaci\u00f3n de un software capaz de reproducir las leyes de transporte de mercanc\u00edas por carretera a partir de las regulaciones de transporte de la Uni\u00f3n Europea, Estados Unidos, Brasil y Canad\u00e1, pa\u00edses en los que el problema tecnol\u00f3gico en este campo se encuentra exactamente en el mismo punto. La metodolog\u00eda para lograr este objetivo consiste en escribir especificaciones formales, en este caso sobre las leyes del transporte, en vez de escribir directamente el software, y en trasladar estas especificaciones a un lenguaje l\u00f3gico-matem\u00e1tico del que se extraer\u00eda el software definitivo sin fallos.<\/p>\n \u201cA trav\u00e9s de este proceso se extrae directamente un programa inform\u00e1tico que garantiza el seguimiento de dichas especificaciones basadas en la ley. La clave que marca la diferencia es que este c\u00f3digo se extrae de demostraciones matem\u00e1ticas. Dichas demostraciones aseguran al cien por cien la correcci\u00f3n del c\u00f3digo con respecto a las especificaciones detalladas al principio del proceso\u201d, detalla Joost Joosten.<\/p>\n Software verificado mediante demostraciones l\u00f3gico-matem\u00e1ticas<\/strong><\/p>\n La metodolog\u00eda parte del paradigma de programaci\u00f3n funcional, que suele utilizarse en los sectores en los que la fiabilidad es cr\u00edtica. Posteriormente, el objetivo es llevar el est\u00e1ndar de seguridad un paso m\u00e1s all\u00e1 y convertir el programa en un c\u00f3digo verificado formalmente, y por tanto sin errores, y certificado mediante un proceso l\u00f3gico-matem\u00e1tico. \u201cLa principal diferencia entre el software verificado formalmente y el software tradicional es que este \u00faltimo se prueba solamente sobre casos particulares, en un proceso que se lleva a cabo a posteriori del desarrollo del programa. En cambio, la verificaci\u00f3n formal tiene como objetivo verificar el conjunto total de ejecuciones posibles del programa. Por eso, el procedimiento por el cual se verifica formalmente un software es totalmente distinto, pues debe acompa\u00f1arle la fuerza de las demostraciones matem\u00e1ticas exactas. De hecho, el c\u00f3digo resultante es el producto de dichas demostraciones, y por lo tanto es un proceso de prueba a priori\u201d, destaca el investigador.<\/p>\n La verificaci\u00f3n formal ha despertado recientemente el inter\u00e9s de la NASA, que pr\u00f3ximamente celebrar\u00e1 su 11\u00ba Simposio sobre M\u00e9todos Formales, y ya se ha implementado en otros proyectos. Uno de los primeros fue el metro de Par\u00eds sin conductor, RATP. Sus informes indican que la verificaci\u00f3n formal del software revel\u00f3 errores que las fases intensivas de pruebas no hab\u00edan revelado antes. Sin embargo, frente a la metodolog\u00eda empleada en Par\u00eds, la de este proyecto, que usa un asistente de demostraci\u00f3n llamado Coq, es m\u00e1s ambiciosa, al ser m\u00e1s costosa pero a la vez m\u00e1s potente, es decir, capaz de llevar la verificaci\u00f3n formal a \u00e1mbitos m\u00e1s complejos. Algunos proyectos de \u00e9xito que usan esta misma metodolog\u00eda son CompCert, un compilador del lenguaje de programaci\u00f3n C verificado formalmente usando Coq, y el sistema operativo eChronos RTOS, verificado formalmente usando el asistente de demostraci\u00f3n Isabelle.<\/p>\n Detr\u00e1s de todas estas t\u00e9cnicas est\u00e1 la teor\u00eda de la demostraci\u00f3n avanzada, que es una rama de la l\u00f3gica matem\u00e1tica. \u201cLo que hacemos es demostrar matem\u00e1ticamente, usando una l\u00f3gica que se llama l\u00f3gica constructiva<\/em>, que existe un algoritmo con tal o cual propiedad, en este caso las especificaciones obtenidas de la ley del transporte. Al hacerlo, el algoritmo extra\u00eddo vendr\u00e1 con un certificado de que cumple con las especificaciones. Este proceso de certificaci\u00f3n es largo, pero todos los pasos que se usan para completarlo son muy simples y la correcci\u00f3n se puede verificar con Coq, un programa que sirve como asistente de demostraci\u00f3n. De esta forma, se comprueban los muchos pero simples pasos que confirman que el software es correcto\u201d, resume Joost Joosten.<\/p>\n Menos burocracia y menos sanciones err\u00f3neas<\/strong><\/p>\n El resultado del proyecto constituir\u00e1 un gran avance, ya que al no producir errores se eliminar\u00e1 la posibilidad de sanciones err\u00f3neas por fallos del software que eval\u00faa los datos del tac\u00f3grafo, lo cual reducir\u00e1 procesos administrativos y judiciales y generar\u00e1 seguridad jur\u00eddica tanto a los profesionales del transporte como a los cuerpos de seguridad de los estados.<\/p>\n Esta iniciativa, que cuenta con un presupuesto total que supera los 2.200.000 euros, est\u00e1 incluida en la convocatoria Retos Colaboraci\u00f3n del Ministerio de Ciencia e Innovaci\u00f3n y Universidades, cuyo objetivo es la financiaci\u00f3n de proyectos en cooperaci\u00f3n entre empresas y organismos de investigaci\u00f3n.<\/p>\n Adem\u00e1s de la Fundaci\u00f3n Bosch i Gimpera de la Universidad de Barcelona, en el consorcio del proyecto tambi\u00e9n participan Guretruck, una empresa que ofrece a entidades servicios de ingenier\u00eda inform\u00e1tica y jur\u00eddica relacionados con el mundo del transporte, y Formal Vindications, una empresa especializada en la verificaci\u00f3n formal de especificaciones t\u00e9cnicas y de software.<\/p>\n Este proyecto, con n\u00famero de expediente RTC-2017-6740-7, est\u00e1 cofinanciado por el Fondo Europeo de Desarrollo Regional (FEDER) de la Uni\u00f3n Europea, cuyo objetivo es promover el desarrollo tecnol\u00f3gico, la innovaci\u00f3n y una investigaci\u00f3n de calidad.<\/p>\n Todos los programas inform\u00e1ticos contienen errores; incluso los que controlan la industria aeron\u00e1utica o militar tienen fallos en el producto…<\/p>\n","protected":false},"author":2,"featured_media":6828,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"inline_featured_image":false,"_monsterinsights_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0,"footnotes":""},"categories":[3],"tags":[],"class_list":["post-6832","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-actualidad"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/posts\/6832","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/comments?post=6832"}],"version-history":[{"count":2,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/posts\/6832\/revisions"}],"predecessor-version":[{"id":8291,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/posts\/6832\/revisions\/8291"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/media\/6828"}],"wp:attachment":[{"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/media?parent=6832"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/categories?post=6832"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.fbg.ub.edu\/es\/wp-json\/wp\/v2\/tags?post=6832"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}![\"\"](\"http:\/\/www.fbg.ub.edu\/wp-content\/uploads\/2019\/02\/MINECO-380x79.jpg\")
\n![\"\"](\"http:\/\/www.fbg.ub.edu\/wp-content\/uploads\/2018\/06\/FEDER_senselema-380x53.jpg\")
<\/p>\n","protected":false},"excerpt":{"rendered":"