Download Presentación - JCC

Algunos Proyectos y
Actividades en Métodos
Formales, en Uruguay.
Instituto de Computación
Facultad de Ingeniería
Universidad de la República
Uruguay
Temario




El Instituto de Computación.
Funciones - Estructura del InCo.
Grupos Académicos y Líneas de
Investigación.
El grupo de Métodos Formales.


Cursos, Proyectos, Algunas actividades en
curso.
Eventos Organizados y Relaciones
Internacionales.
El InCo

El Instituto de Computación (InCo) es uno de
los departamentos de la Facultad de Ingeniería.
Instituto de Computación
Datos Generales

Universidad de la República:




Única universidad pública uruguaya,
Creada a mediados del siglo XIX,
Organizada en Facultades.
Instituto de Computación:




Instalado en 1966 y "re-fundado" en 1985.
Único instituto de la UDELAR dedicado al área
informática / computación.
Parte de la Facultad de Ingeniería.
Vinculado con el PEDECIBA - Programa de
Desarrollo de las Ciencias Básicas.
Funciones del InCo

Docencia:


Reponsable de carrera Ing. en Computación.
Postgrados:



Investigación:


Perfil académico:
 Maestría (’89) y Doctorado (‘97) : junto con el PEDECIBA.
Perfil aplicado / profesional: Maestría (‘2000).
Grupos especializados en áreas académicas.
Vinculación con el medio e industria:



Asesoramientos a empresas.
Cursos para profesionales (postgrado y formación
permanente).
Emprendimientos conjuntos con sector empresarial.
Personal

Integrantes:



120-130 docentes; 40% de media/alta dedicación, 60%
de baja dedicación. 20% son contratados por proyectos.
aproximadamente 40-50% con formación de postgrado.
(1/3 con Doctorado y 2/3 con Maestría)
Formaciones ofrecidas:




Ingeniero en Computación (5 años) – 500 ingresos/ año.
Magister en Ingeniería de Computación (2 años) – 25
ingresos cada 18 meses.
Magister en Informática (2 años) – 10 ingresos/ año.
Doctorado en Informática (3 años) – 3 ingresos/ año.
Carrera de Ing. Computación

Duración:


Bloques:



10 “semestres” de 16 semanas c/u.
1o a 3er año: cursos obligatorios.
4o y 5o año: opcionales.
Cantidades de estudiantes:

Ingresan 500 estudiantes a Computación.




La mitad de los ingresos a la Fac. de Ingeniería.
Aprox. 1300 estudiantes en 1er. año.
Egresan aprox. 200 Analistas en Computación (3er año).
Egresan aprox. 70 Ingenieros en Computación.
Investigación

Las actividades de investigación y
asesoramiento técnico especializado se
organizan en torno a los distintos grupos
académicos que funcionan en el
Instituto.
Grupos Académicos







Laboratorio de Ciencias de la Computación
(Grupo de Métodos Formales)
Procesamiento de Lenguaje Natural
Investigación de Operaciones
Centro de Cálculo
Sistemas de Información
Ingeniería de Software
Arquitectura, Redes y Comunicaciones
Grupos Académicos (1)

Laboratorio de Ciencias de la Computación

Areas de trabajo:









Anlálisis de Algoritmos y Criptografía.
Teoría de la Información.
Métodos Formales.
Lenguajes de Programación.
Arquitecturas de Software, POO, POA.
Enseñanza de Programación.
Seguridad Informática.
Responsable: Dr. Alberto Pardo ([email protected]).
Grupo Procesamiento de Lenguaje Natural

Areas de trabajo:




Extracción de información de textos.
Bases de datos de texto.
Transductores; Web Semántica.
Responsable: Dra. Dina Wonsever ([email protected]).
Grupos Académicos (2)

Departamento Investigación de Operaciones

Areas de trabajo:






Planificación de redes globales.
Optimización, Logística y Transporte.
Simulación.
Management Sciences.
Responsable: Prof. Omar Viera ([email protected]).
Grupo Centro de Cálculo

Areas de trabajo:




Interfases Hombre-Máquina.
Tratamiento de Imágenes.
Métodos Numéricos y Cálculos de alta performance.
Responsable: Prof. Eduardo Fernandez
([email protected]).
Grupos Académicos (3)

Grupo Sistemas de Información

Areas de trabajo:





Data Warehouses.
Web Semántica y Web Services Semánticos.
Integración de Sistemas y Middleware.
Responsable: Dra. Regina Motz ([email protected]).
Grupo Ingeniería de Software

Áreas de trabajo:



Procesos de desarrollo de software.
Técnicas de verificación de software.
Responsable: Prof. Jorge Triñanes ([email protected]).
Grupos Académicos (4)

Grupo Arquitectura, Redes y Comunicaciones

Áreas de trabajo:





Calidad en comunicaciones.
Redes de alta velocidad.
Redes inalámbricas.
Grid.
Responsable: Dr. Eduardo Gampin ([email protected]).
Laboratorio de Cs. de la Computación.
Integrantes

Profesores Titulares (Gr.5)


Profesores Agregados (Gr.4)


Betarte, Gustavo; Pardo, Alberto; Tasistro, Alvaro.
Profesores Adjuntos (Gr.3)


Cabezas, Juan José; Viola, Alfredo.
Bove, Ana; Calderon, Guillermo; Da Rosa, Sylvia;
Luna, Carlos; Sierra, Luis; Vignaga, Andres.
Asistentes (Gr.2)

Gustavo Brown, Calegari, Daniel; Corral, Jorge;
Dominguez, Facundo; Martin, Alvaro; Martinez,
Mónica; Perovich, Daniel; Rivero, Diego;
Rodriguez, Leonardo; Viera, Marcos.
Laboratorio de Cs. de la Computación

Docencia, cursos (1):





Lógica.
Verificación y Lógica.
Modelos y verificación de sistemas de
tiempo real.
Lógica de la programación imperativa.
Construcción formal de programas en teoría
de tipos (TPPSF).
Laboratorio de Cs. de la Computación.
Grupo de Métodos Formales

Docencia, cursos (2):








Asignaturas de programación (P1,P2,P3,P4).
Introducción a la programación funcional.
Programación genérica.
Análisis de algoritmos.
Introducción a la criptografía.
Seguridad.
Programación para diseño gráfico.
Diseño de compiladores.
Laboratorio de Cs. de la Computación.
Grupo de Métodos Formales

Proyectos (1):


Deforestación en Presencia de Efectos, PDT Uruguay (20042006).
(Alberto Pardo - Fusión de Programas).
Técnicas de transformación de programas basadas en fusión
(en evaluación, PDT Uruguay, 2007-2008).
El objetivo de este proyecto es continuar y profundizar el estudio de
aspectos teóricos y prácticos de la técnica de fusión de programas
funcionales.


Modelar esquemas de recursión y estudiar sus
propiedades algebraicas relevantes para la fusión de programas.
desarrollo de nuevas extensiones para la herramienta HFusion.


Incrementar el poder de fusión de la herramienta mediante la
incorporación de nuevos casos de fusión que pueda resolver.
Estudiar la efectividad práctica de la herramienta, para lo cual se propone
analizar la forma de incorporarla al compilador GHC de Haskell.
Laboratorio de Cs. de la Computación

Proyectos (2):


Estudio de Modelos para Procesos
Estocásticos de Memoria Finita, CSIC
Uruguay (2004-2006).
(Alfredo Viola - Teoría de la Inf., AA).
...
Laboratorio de Cs. de la Computación.
Grupo de Métodos Formales

Proyectos (3):

Verificación de Sistemas Críticos: de la
Especificación al Código, PDT Uruguay
(2006-2007)
(Carlos Luna y Luis Sierra)
Laboratorio de Cs. de la Computación.
Grupo de Métodos Formales

Proyectos (4):

ReSeCo: Reliability and Security of
Distributed Software Components, TICAMSUD Francia-Argentina-Chile-Uruguay
(2006-2008)
(Gustavo Betarte, Carlos Luna, Luis Sierra)

Objetivo principal: investigar la seguridad y fiabilidad en un
modelo computacional, donde tanto las plataformas como
las aplicaciones son dinámicas, de forma que componentes
provistos por un agente externo puedan ser destinados a
formar parte de la plataforma o ejecutar una aplicación de
forma segura.
Laboratorio de Cs. de la Computación.
Grupo de Métodos Formales

Proyectos (5):

STEVE: Seguridad a Través de Evidencia
VErificable, PDT Uruguay (en evaluación,
2007-2008)
(Gustavo Betarte y Carlos Luna)


Proyecto inserto en los objetivos de ReSeCo
Otros proyectos: ...
Algunas Actividades en
curso... (1)

Especificación de sistemas reactivos y de
tiempo Real.


Lenguajes de modelado + Lógicas.
Metodologías que combinen enfoques y
herramientas.


C. Luna. "Model Checkers" + "Proof Assistants" en la Verificación
de Sistemas de Tiempo Real. SPL2006 - II Southern Conference
on Programmable Logic, 2nd SURLabs - Regional Joint LatinAmerican Laboratories on FPGA Technology, March 2006 - Mar
del Plata, Argentina.
Especificación y verificación de un PIC.


Formalización y razonamiento a bajo nivel.
Relación entre el bajo y el alto nivel.
Algunas Actividades en
curso... (2)

Formalización de Lógicas en Coq.
(sistemas reactivos y de tiempo real)

CTL, TCTL ((Timed) Computation Tree Logic).





Bibliotecas disponibles en el proy. Coq.
Análisis de casos de estudio.
ATL (Alternating-time temporal logic).
Álgebras de procesos con (y sin) tiempo.
Experiencias de Luis...
Algunas Actividades en
curso... (3)
Formalización de políticas de seguridad
para dispositivos móviles.


A Formal Specification of the MIDP 2.0
Security Model (S. Zanella, G. Betarte, C.
Luna)


S. Zanella Béguelin. Especificación formal del modelo de
seguridad de MIDP 2.0 en el Cálculo de Construcciones
Inductivas. Tesina de Grado, Universidad Nacional de Rosario,
Mayo de 2006.
S. Zanella Béguelin, G. Betarte, and C. Luna. 4th International
Workshop on Formal Aspects in Security and Trust, FAST 2006,
Hamilton, Canada, August 26-27 2006, Lectures Notes in
Computer Science. Springer 2006. To appear.
Algunas Actividades en
curso... (4)

Formalización de políticas de seguridad
para dispositivos móviles. Propuestas.

A Formal Specification of the MIDP 2.0
Security Model (S. Zanella, G. Betarte, C.
Luna)

Trusted Midlet Suites. Esta actividad tiene como objetivo
principal especificar el procedimiento de verificación y
autorización de instalación de una midlet suite en un dispositivo
móvil, según el authorization model definido en el capítulo 3 de
[MIDP2.0] “Security for MIDP Applications”.

ACDM. Este trabajo consiste en el modelado, prueba de
propiedades, y derivación de una implementacion correcta de un
Access Control Decision Module (ACDM) para MIDP 2.0.
Algunas Actividades en curso...
(5) http://www.fing.edu.uy/~pardo.




Estudio de esquemas de recursión para programas
puramente funcionales y programas funcionales con
efectos.
Estudio de leyes de fusión para estos esquemas.
Estudio de mecanismos para modelar efectos en
programación funcional (mónadas, comónadas, etc).
Desarrollo de HFusion, una herramienta para la fusión
de programas Haskell.
(http://www.fing.edu.uy/inco/proyectos/fusion/tool/).



"Automatización de Leyes de Fusión de Programas". Facundo Domínguez y
Alberto Pardo. CLEI 2006, Santiago, Chile, Agosto 2006.
"Program Fusion with Paramorphisms". Facundo Domínguez y Alberto Pardo.
Workshop on Mathematically Structured Functional Programming (MSFP'06),
Kuressaare, Estonia, Julio 2006.
"Combining Datatypes and Effects". Alberto Pardo. Advanced Functional
Programming, Lecture Notes in Computer Science Vol. 3622, 2005.
Algunas Actividades en
curso... (6)

Algunas otras líneas dentro del grupo:

Enseñanza de programación y ciencias de la computación
(Sylvia da Rosa).




The learning of recursive algorithms and their functional
formalization.
Una Semántica Formal de Interacciones UML 2.0 con Soporte
para Restricciones Temporales (Daniel Calegari).
A Multi-Stage Language with Intensional Analysis, Generative
Programming and Component Engineering (Marcos Viera)
…
Relaciones Internacionales (1)

Argentina - Universidad de Rosario.




Colombia – Universidad de CAUCA:


Sistemas de Información Federados.
Brasil – UFMG (Univ. Federal de Minas Gerais)



Sistemas de Información.
Investigación Operativa.
Métodos Formales.
Programación funcional.
Métodos formales.
Brasil – Univ. Federal de RG do Sul.


Sistemas de Información.
Procesamiento de Lenguaje Natural.
Relaciones Internacionales (2)

España - UP Catalunya:



Portugal: la Univ. do Minho



Programación funcional.
Métodos formales.
Iberoamérica:


Sistemas, Redes y Comunicaciones.
Tratamiento de Imágenes.
Redes y proyectos CYTED.
Francia:

Lab. PRiSM – Versailles.

Sistemas de Información.
Relaciones Internacionales (3)

INRIA.




Univ. Paris IV.


Tratamiento Lenguaje Natural.
Canada:



SmartCards, Seguridad -Métodos Formales- (Sophia
Antipolis).
Redes (Rennes).
Verificación de programas (Rocquencourt).
Universidad de Carleton.
Universidad de Ottawa.
EEUU:


HP Labs.
Microsoft Research.
Cooperación Internacional (4)



Proyectos y redes CYTED.
Proyectos ALFA.
Proyecto EU @LIS.
Algunos eventos organizados

XIII CLAIO









Congreso Latino-Iberoamericano de Investigación Operativa
Montevideo, Uruguay. 27 al 30 de noviembre de 2006.
Tercer Campeonato Uruguayo de Sumo Robótico
 Montevideo, Uruguay. 30 de octubre 2006.
ITW’2006
 IEEE Information Theory Workshop. Punta del Este. Marzo 2006
ICIL 2005 (Int. Conf. on Industrial Logistics).
LPAR 2004 (Logic for Programming, AI and Reasoning).
WSSA 2003 (International Winter School on Semantics and
Applications).
CLEI 2002.
LATIN 2000 (LA Conf. In Theo. Informatics).
IV and X ELAVIO (LA Summer School on Op. Research), 1997, 2004.
Rel.Int. : Oferta

Emprendimientos con el sector empresarial.

Centro de Ensayos de Software (CES).



Ofrece servicios de validación (testeo) de software.
Consorcio con la CUTI.
Centro Académico-Industrial en TI (CAITI).


Convenio a nivel nacional entre CUTI, Gobierno y
Universidades (+PNUD).
Objetivo: impulsar desarrollo conjunto Academia-Industria.
Contactos e inform. en web



Página web la Facultad de Ingeniería: www.fing.edu.uy
Página web del InCo: www.fing.edu.uy/inco
Página web de MF: www.fing.edu.uy/inco/grupos/mf








Gustavo Betarte: http://www.fing.edu.uy/~gustun
Carlos Luna: http://www.fing.edu.uy/~cluna
Alberto Pardo: http://www.fing.edu.uy/~pardo
Luis Sierra: http://www.fing.edu.uy/~sierra
…
PEDECIBA : www.rau.edu.uy/pedeciba/informat
CAITI : www.caiti.org.uy
CES : www.ces.com.uy
Agradecimientos
A Raúl Kantor, a Cecilia Manzino y a Dante Zanarini por
hacer posibles las actividades entre la UNR (Argentina)
y la UDELAR (Uruguay) desde 2005, en el área de
métodos formales.