Conceptos de model checking

Docente:

Dr. Pedro R. D'Argenio.

Resumen:

Este curso se enfocará en la verificación automática de modelos de sistemas concurrentes en general, incluyendo modelos para sistemas reactivos, sistemas embebidos, sistemas distribuidos, redes y protocolos, sistemas de tiempo real, etc.

Se enseñará los conceptos semánticos básicos para comprender estos tipos de sistemas. Comenzaremos por estudiar análisis de deadlocks e invariantes. Luego introduciremos propiedades de safety y su análisis a través de lenguaje regulares y autómatas finitos y a continuación propiedades de fairness y su análisis utilizando lenguajes ω-regulares y autómatas de Büchi.  Utilizaremos la lógica temporal lineal (LTL) como lenguaje de especificación de propiedades y daremos el algoritmo para realizar model checking de esta lógica.

El curso finalizará con una rápida revisión de otras técncas y técnicas más avanzadas, incluyendo la lógica CTL, BDDs, técnicas de abstracción, model checking de sistemas temporizados y de sistemas probabilistas entre otras cosas.

Horario: de 11 a 13:30 hs.

Lugar: Anfiteatro 1 del Pabellón 2.

Slides y ejercicios.

porn sites
live cam sex
logolu peçete