Tribunal

Hoy fuí por 1º vez parte de un tribunal para evaluar una tesis. Por suerte fue un muy buen trabajo y fue fácil poner un 10. Los detalles técnicos:


Alumno: Carlos S. Bederián
Director: Pedro D'Argenio.

Título: Model checking cuantitativo de propiedades LTL en PRISM

Auditorio, Viernes 4 de julio a las 16:00 hs.

Resumen:

Las técnicas de verificación formal de sistemas complementan a las técnicas de testing en el proceso de desarrollo, y son imprescindibles para asegurar la corrección de sistemas críticos cuyos fallos pueden tener resultados catastróficos.

En este trabajo agregamos soporte para verificar propiedades en la lógica temporal LTL sobre modelos con elementos probabilistas y no deterministas a la herramienta de model checking PRISM [1], utilizando el algoritmo descrito por Luca de Alfaro en [2] que reduce el problema a un cálculo de alcanzabilidad máxima.

Como el model checking sufre de baja escalabilidad cuando se utilizan representaciones explícitas del modelo, el algoritmo ha sido convertido en su totalidad al uso de diagramas de decisión binarios [3], una estructura de datos optimizada para almacenar grandes modelos en una cantidad pequeña de memoria sin sacrificar demasiada performance para operar sobre el mismo.

[1] http://www.prismmodelchecker.org/

[2] Luca de Alfaro. Temporal Logics for the Specification of Performance and Reliability. Lecture Notes in Computer Science, 1200:165—176, 1997.

[3] Randall Y. Bryant. Symbolic boolean manipulation with ordered binary decision diagrams. Technical report, CMU, 1992.