modified on 21 jul 2017 at 00:39 ••• 9.300 views

Razonamiento Asistido por Computador

De Master

(Diferencias entre revisiones)
(Programa de la asignatura)
(Página Web)
Línea 12: Línea 12:
== [http://www.us.es/estudios/master/master_M095/asignatura_50950011 Programa de la asignatura] ==
== [http://www.us.es/estudios/master/master_M095/asignatura_50950011 Programa de la asignatura] ==
-
== [http://www.cs.us.es/~jalonso/cursos/m-ra/ Página Web] ==
+
== [http://www.cs.us.es/cursos/ram/ Página Web] ==

Revisión de 02:27 21 feb 2013

Contenido

En la actualidad, los sistemas de hardware y de software tienen con frecuencia un grado de complejidad elevado, y la tendencia es que cada vez sean más complejos. Algunos de estos sistemas son denominados "de seguridad crítica", ya que su corrección (es decir, que funcionen como se espera que funcionen) es fundamental (por ejemplo, porque de ellos dependan vidas humanas o grandes cantidades de dinero). La aproximación clásica a la verificación de la corrección consiste en comprobar el sistema sobre un conjunto grande de datos de entrada. Si bien este método puede ser satisfactorio en algunos casos, no lo es en el caso de los sistemas de seguridad crítica, ya que el descubrimiento de un fallo está supeditado a que el dato de entrada que lo desvela se encuentre en el conjunto de las pruebas. Una alternativa consiste en modelar formalmente los sistemas como objetos matemáticos, y formular su corrección mediante teoremas, susceptibles de ser demostrados formalmente. De esta manera aumentamos drásticamente nuestra confianza en su buen funcionamiento. La complejidad de los sistemas puede hacer que esas demostraciones sean laboriosas y complejas, por lo que resulta imprescindible disponer de la ayuda de un sistema que sirva para comprobar las demostraciones. ACL2 es uno de los sistemas de razonamiento automático se ha aplicado en la industria, sobre todo para la verificación de hardware.

Los objetivos de esta materia son los siguientes:

  • Conocer la aproximación formal a la verificación de sistemas, tanto hardware como software.
  • Entender el modelado de sistemas en un lenguaje formal, y en particular manejar el lenguaje de programación de ACL2 como medio de expresión para realizar los modelos.
  • Conocer la lógica de ACL2, su axiomas , sus reglas de inferencia (con especial énfasis en el principio de inducción) y la noción de demostración en la misma.
  • Entender el funcionamiento del demostrador automático de ACL2, como asistente en la realización de pruebas formales de la corrección de los sistemas modelados.
  • Alcanzar destreza práctica en el manejo del demostrador para la demostración de resultados sencillos.

Programa de la asignatura

Página Web