Escuela de Capacitación ICTAC 2023 en Métodos Formales Aplicados
Sobre la Escuela de Capacitación
Métodos Formales son técnicas basadas en lógica para la especificación, desarrollo y verificación de sistemas. Contribuyen a la confiabilidad de sistemas y usan modelos de sistemas que capturan sus aspectos dinámicos (por ejemplo, procesos, transiciones) y sus propiedades (por ejemplo, ‘safety’, ‘liveness’, ‘fairness’).
La escuela de capacitación ICTAC 2023 en métodos formales aplicados se realizará en Lima - Perú en la UTEC, del 04 al 05 de diciembre de 2023 y está dirigida a estudiantes de maestría, estudiantes de doctorado, investigadores y profesores en el campo de la informática y las matemáticas que no están familiarizados con métodos formales y quieren tener una idea de qué son los métodos formales. Planeamos hacerlo a través de varias clases magistrales en métodos formales seleccionados.
Existe un número limitado de inscripciones gratuitas, auspiciados por SIGSOFT, y un número limitado de inscripciones con pago mínimo para residentes/ciudadanos peruanos. Por favor contacte a Cristian López del Álamo (clopezd@utec.edu.pe) para mayor información. Porfavor traer sus laptops ya que la mayoria de las clases son practicas. Las clases se dictaran en ingles.
Adicionalmente, se realizaran en paralelo una serie de tutoriales avanzados, mas información aquí. El programa completo de ICTAC 2023 se encuentra aquí.
Ponentes
Nombre: Pedro R. D'Argenio
Afiliación: Universidad Nacional de Córdoba, Argentina
Página personal: https://cs.famaf.unc.edu.ar/~dargenio/
Biografía:
Pedro R. D'Argenio es Profesor Titular de Informática de FAMAF, Universidad Nacional de Córdoba.
También ocupa un puesto de investigación en el CONICET. Estudió informática en la Universidad Nacional de La Plata (Argentina) y obtuvo su Ph.D.
en la Universidad de Twente (Países Bajos) donde también realizó su postdoctorado.
También trabajó en la Université de Provence (FR) y fue profesor invitado en la Universidad de Twente (NL) y la Universidad del Sarre (DE).
Es ex Director del Programa de Doctorado en Ciencias de la Computación y ex Decano Asociado de Ciencia y Tecnología de FAMAF, UNC.
Actualmente es el presidente del IFIP WG 1.8 sobre Teoría de la Concurrencia. El Profesor D'Argenio es un investigador líder en técnicas
formales para sistemas confiables y contribuye en áreas como verificación de modelos (model checking), semántica de procesos,
tolerancia a fallas, seguridad y testeo.
Ha liderado y participado en numerosos proyectos de investigación argentinos y europeos.
Probabilistic Model Checking.
Fecha y hora: 4 de Diciembre 2023, 09:00 - 12:30
Model Checking es una herramienta poderosa para chequear automáticamente si un modelo satisface una propiedad determinada.
Normalmente proporcionan una respuesta Booleana a una pregunta cualitativa.
Sin embargo, las características probabilísticas normalmente aparecen en sistemas que generalmente tienen características cruciales.
Por ejemplo, es común utilizar protocolos aleatorios para resolver situaciones de contención en redes o para comprender modelos de fallas
a través de comportamientos estocásticos de las fallas. En este último caso, por ejemplo, la afirmación "el sistema no falla" podría ser
imposible de chequear, mientras que la pregunta apropiada podría ser "el 99% de las veces el sistema no falla".
En esta clase introduciremos los fundamentos y algoritmos para abordar el chequeo de este tipo de propiedades cuantitativas.
En particular, hablaremos sobre el chequeo de propiedades cuantitativas y cualitativas en cadenas de Markov de tiempo discreto,
así como el entorno más versátil con el proceso de decisión de Márkov.
Clase patrocinada por The ICT faculty at The University of Malta
Nombre: Christian Colombo
Afiliación: Universidad de Malta, Malta
Página personal: https://www.um.edu.mt/profile/christiancolombo
Biografía:
Christian Colombo obtuvo su Ph.D. en Ciencias de la Computación de la Universidad de Malta en 2013 y actualmente ocupa el puesto de Profesor Asociado dentro del Departamento de Ciencias de la Computación. Sus principales áreas de investigación son la verificación en tiempo de ejecución, testeo de software, transacciones de compensación y lenguajes de dominios específicos, centrándose en la creación de sistemas de software confiables verificándolos con especificaciones formales en tiempo de ejecución. Las aplicaciones de este conjunto de investigaciones abarcan la seguridad de dispositivos móviles, sistemas de pasarelas de pago, políticas de privacidad de redes sociales y cumplimiento tributario, entre otros. Participa activamente en actividades de divulgación tanto a nivel de departamento como de facultad, interactuando con futuros estudiantes potenciales, la industria y el público en general. Ha estado estrechamente involucrado en una serie de proyectos financiados: Confiabilidad y recuperación de errores en sistemas financieros intensivos en seguridad [MCST] (2008-2011), Ecosistema de pagos abiertos [H2020] (2015-2017), Generación automática de monitores en línea a partir de pruebas [ MCST] (2015-2017); LOCARD [H2020-SU-SEC-2018: 832735] (2019-2022), Comunicación Segura en la Era Cuántica [Número de Proyecto SPS: G5448] (2018-2022), y DETECTIF [MCST REP-2022-007] (2022- 2023).
La teoría y práctica de la verificación en tiempo de ejecución:
Una introducción práctica a la técnica de métodos formales con aplicaciones en el monitoreo de la seguridad cibernética.
Fecha y hora: 4 de Diciembre 2023, 14:00 - 17:30
La verificación en tiempo de ejecución es una técnica de métodos formales livianos que sintetiza monitores ejecutables a partir de descripciones de comportamiento no ambiguos. Dichos monitores luego se combinan automáticamente con el sistema bajo escrutinio para verificar su comportamiento correcto en tiempo de ejecución. Basándose en dos décadas de experiencia, esta sesión comenzará cubriendo las bases teóricas de la verificación en tiempo de ejecución, en particular la especificación y detección de cualquier infracción de comportamiento en tiempo de ejecución. A continuación, tendremos una sesión práctica en la que se invitará a los participantes a probar el código Java y AspectJ en sus IDE, utilizando un estudio de caso de transacción financiera (consulte el libro https://github.com/ccol002/rv-book para mas información). La última parte de la sesión se centrará en la verificación de tiempo de ejecución en el contexto de la ciberseguridad; mostrando cómo puede monitorear la ejecución de protocolos de seguridad, imponer el aislamiento de un entorno de ejecución confiable y extraer evidencia que de otro modo sería difícil de obtener.
Nombre: Marijn J.H. Heule
Afiliación: Universidad Carnegie Mellon, Estados Unidos de América
Página personal: https://www.cs.cmu.edu/~mheule/
Biografía:
Marijn Heule es Profesor Asociado de Ciencias de la Computación en la Universidad Carnegie Mellon. Sus contribuciones al razonamiento automatizado le han permitido a él y a otros investigadores resolver problemas difíciles en verificación formal y matemática. Ha desarrollado solucionadores de satisfacibilidad (SAT) galardonados. Sus técnicas de preprocesamiento y producción de pruebas se utilizan en muchas herramientas de razonamiento automatizadas de última generación. Marijn ha ganado múltiples premios al mejor artículo en conferencias internacionales, incluidas SAT, CADE, IJCAR, TACAS, HVC, LPAR e IJCAI-JAIR. Es uno de los editores del 'Handbook of Satisfiability'. Este manual de más de 1500 páginas (segunda edición) se ha convertido en la referencia para la investigación de SAT.
Resolución de satisfacción (satisfiability solving).
Fecha y hora: 5 de Diciembre 2023, 09:00 - 12:30
Los solucionadores de satisfacibilidad (SAT) se han convertido en potentes motores de búsqueda para resolver una amplia gama de aplicaciones en campos como la verificación formal, la planificación y las matemáticas. Esta sesión sobre resolución de SAT consta de dos partes. La primera parte se centra en una introducción que abarca desde muchas aplicaciones del SAT hasta interesantes aspectos teóricos. También cubre técnicas básicas de resolución. La segunda parte proporciona experiencia práctica sobre cómo utilizar los solucionadores SAT en la práctica. Esta parte consta de varios ejemplos, incluyendo cómo codificar un problema de coloración de gráficos en SAT y resolver la fórmula resultante con un solucionador automático de primer nivel. Además, mostraremos algunas herramientas para facilitar el uso de SAT. Concluimos presentando los solucionadores de la teoría del módulo de satisfacibilidad (satisfiability modulo theory - SMT) y cómo se pueden utilizar para resolver problemas.
Clase patrocinada por FME (Formal Methods Europe) y
The University of York
Nombre: Ana Cavalcanti
Afiliación: Universidad de York, Reino Unido
Página personal: https://www-users.york.ac.uk/~alcc500/
Biografía:
Ana Cavalcanti es Profesora Titular de la Universidad de York y poseedora del premio Wolfson Research Merit Award de la Royal Society. En 2003, recibió una beca industrial de la Royal Society para trabajar con QinetiQ en métodos formales. Ha publicado más de 100 artículos y presidió el Comité de Programa de varias conferencias internacionales reconocidas. Su principal interés de investigación es la teoría y práctica de los métodos formales. Ella ha contribuido en temas tales como refinamiento, sistemas críticos para la seguridad, la orientación a objetos, la concurrencia y las aplicaciones en tiempo real. Ha desempeñado un papel importante en el diseño y formalización de un álgebra de procesos rico en estados, conocido como Circus, y sus técnicas de desarrollo utilizan las teorías unificadoras de programación de Hoare y He.
Nombre: Ziggy Attala
Afiliación: Universidad de York, Reino Unido
Página personal: https://www.cs.york.ac.uk/people/?username=ziggy
Biografía:
Ziggy Attala actualmente está terminando su doctorado en la Universidad de York. Su tema de tesis se centra en la verificación de modelos RoboChart con componentes integrados de redes neuronales artificiales. Sus asesores son Ana Cavalcanti y Jim Woodcock. Su tesis de pregrado, fue asesorada por Arno Pauly en la Universidad de Swansea, se centró en cómo los modelos de aprendizaje automático (machine learning) pueden aprender y reconocer otros modelos de aprendizaje automático. Sus intereses de investigación incluyen métodos formales, machine learning, y la verificación de redes neuronales artificiales.
Nombre: Jim Woodcock
Afiliación: Universidad de York, Reino Unido
Página personal: https://pure.york.ac.uk/portal/en/persons/jim-woodcock
Biografía:
Jim Woodcock es Profesor Titular, muy reconocido en el area de ingeniería de software en la Universidad de York, es miembro de la Real Academia de Ingeniería, ingeniero colegiado, profesional colegiado de TI e investigador y profesor galardonado. También es profesor de Ingeniería de Software de Robots Móviles y Autónomos en la Universidad de Aarhus y Profesor de Sistemas Ciberfísicos en la Universidad del Sudoeste de China. Tiene 45 años de experiencia en métodos formales y ha dedicado su carrera investigadora a la búsqueda de los principios matemáticos que son esenciales para la práctica de la ingeniería de software. Sus intereses de investigación específicos están en las teorías unificadoras de programación (UTP), robótica, gemelos digitales y aplicaciones industriales. Dirige el equipo que crea teorías UTP para programación concurrente rica en estados, incluidos tiempos y probabilidades, y está desarrollando el demostrador de teoremas de Isabelle/UTP. Aplicó la notación Z al proyecto IBM CICS, lo que ayudó a obtener el 'Queen's Award for Technological Achievement'. Creó la verificación teórica y práctica para el sistema de tarjetas inteligentes Mondex de NatWest Bank, el primer producto comercial que alcanza el nivel E6 de ITSEC (Criterios comunes EAL 7). Durante la última década, ha investigado la teoría y la práctica de los sistemas ciberfísicos y la robótica, y recientemente, su semántica probabilística. Es editor en jefe de la revista ACM Formal Aspects of Computing y editor en jefe de la revista CUP Research Directions: Cyber-Physical Systems.
Ingeniería de Software para Robótica: tecnología RoboStar.
Fecha y hora: 5 de Diciembre 2023, 14:00 - 17:30
El uso de simulaciones para respaldar el diseño de software para sistemas robóticos es generalizado. Normalmente, los expertos en robótica dibujan una máquina de estados utilizando una notación informal (no precisa ni verificable por una computadora) para transmitir un diseño y guiar el desarrollo de una simulación. Esto implica escribir código para un simulador específico (usando C, C++ o algún lenguaje propietario y API). Los simuladores de robótica reactiva normalmente no generan código para su implementación. En cambio, el código de simulación a menudo se reutiliza después de varios cambios. Por lo tanto, existe una pérdida potencial de propiedades observadas mediante la simulación: debido a la posibilidad de que los cambios introduzcan errores y debido a la brecha de la realidad. La tecnología RoboStar mantiene un enfoque de desarrollo basado en modelos, en lugar de código (simulación). Los modelos se escriben utilizando notaciones específicas de dominio conforme con las aceptadas por los expertos en robótica. En esta sesión, nos centraremos en el modelado y la verificación utilizando RoboChart, nuestra notación de diseño y sus herramientas. En RoboChart, los controladores de software se describen mediante máquinas de estado cronometradas. La semántica se define mediante un álgebra de procesos, concretamente, tock-CSP , que utilizamos para la verificación.