Conceptos de Model Checking
La Escuela de Verano de Ciencias Informáticas se realiza anualmente desde 1994, organizada por el Departamento de Computación, de la Facultad de Ciencias Exactas Físico-Químicas y Naturales de la Universidad Nacional de Río Cuarto (UNRC). Los principales objetivos de la escuela son:
- Brindar a los alumnos y docentes de las carreras de computación de la UNRC, de otras universidades nacionales y a toda la comunidad informática, cursos intensivos y breves de actualización y especialización dictados por docentes e investigadores de primer nivel.
- Poner al alcance de los alumnos de las carreras de computación de la UNRC una visión amplia y diversa del campo de las Ciencias Informáticas y facilitar el intercambio académico con otras casas de estudio.
- Promover la participación de los alumnos de las carreras de Computación de la UNRC en otros eventos similares en Universidades del país y del extranjero.
La Rio 2019, 26º Escuela de Verano de Ciencias Informáticas se realizó entre el 18 y el 23 de febrero de 2019 en el campus de la UNRC y tuve el placer de ser invitado a dictar uno de los cursos.
Titulo del curso: Conceptos de Model Checking.
Resumen: Este curso se enfocará en la verificación automática de modelos des 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.