• Actividad Calificable (AC1): Modelado del sistema a partir de requisitos no formales. Se trata de recordar la notación no formal de los DTE. Se proponen una serie de sistemas con unos requisitos funcionales y el alumno debe crear un primer modelo jerárquico del sistema utilizando alguna notación tipo DTE.
• Actividad Calificable (AC2): La lógica como lenguaje de especificación. Se trata de saber expresar enunciados sencillos mediante expresiones de lógica clásica. Esto incluye la lógica proposicional y la predicativa. La instalación y uso de sencillos ejemplos con la herramienta Alloy.
• Actividad Calificable (AC3): Especificación de sistemas temporales. Con las lógicas temporales se consigue expresar y modelar sistemas de tiempo real. Se tratará de expresar requisitos en algún sistema de verificación formal y saber interpretar el resultado.
• Actividad calificable (AC4): Verificación de programas.  Entender el mecanismo de la verificación formal de requisitos. Consiste en la resolución de ejercicios tipo con varias especificaciones. Se utiliza la notación de Hoare.

• AC1: Modelado del sistema a partir de requisitos no formales. Se evalúa la capacidad de abstracción para comprender un problema y utilizar una notación capaz de modelar el sistema acorde con la especificación dada.
• AC2: La lógica como lenguaje de especificación. Se evaluará la destreza en el uso de las expresiones lógicas para transmitir y reflejar ciertas características o restricciones del modelo. Se evaluará también el uso del programa Alloy.
• AC3: Especificación de sistemas temporales. Continuando con el estudio de la lógica se evaluará la capacidad y destreza del alumno para modelar mediante lógicas temporales ciertos sistemas reactivos. El uso y destreza de verificadores formales como NuSMV
• AC4: Verificación de programas.  Se evaluará la destreza para traducir especificaciones al formato de Hoare y saber realizar pruebas de correcciones parciales.
• ANC: Lógica modal.  Se pretende que el alumno adquiera destreza en la descripción de un sistema multi agente. Ello requiere saber utilizar la notación de lógicas modales.

Como criterios generales y comunes a todos los trabajos se tendrá en cuenta:

- La capacidad para argumentar y transmitir adecuadamente las ideas y conceptos de la asignatura. 

- La participación activa en los foros de discusión del curso.

- La ética y honestidad a la hora de presentar  trabajos originales con aporte de ideas propias que mejoren o generalicen las soluciones presentadas. 

Si falta alguna Actividad Calificable en la convocatoria de Junio no se podrá calificar como apto en esta convocatoria.

No obstante, los trabajos que falten, o hayan sido evaluados de forma insuficiente, se podrán entregar para su evaluación en la convocatoria Extraordinaria de Septiembre.

La calificación de los trabajos aprobados se mantiene en la convocatoria extraordinaria.

Si todos los trabajos están aprobados, esto es, cada uno tiene una calificación >= 5, entonces

la Nota Final se obtiene de la media aritmética de todas las Actividades Calificables.