Laboratório de Métodos Formais (Opção 5.º ano)
[ DI/UM ]

Novo	Classificações 2006/7 (época especial) -- ver 2006/07

[ Contacto | Informações Gerais | Objectivo | Regime de Avaliação | Cursos
2006/07
2005/06 | 2004/05 | 2003/04 | 2002/03 | 2001/02 | 2000/01 | 1999/00 ]

  Cursos

5309V7

- Opção IV - Licenciatura em Engenharia de Sistemas e Informática, 5.º ano

7009T2

- Opção VI - Licenciatura em Matemática e Ciências da Computação, 5.º ano

7009U2

- Opção V - Licenciatura em Matemática e Ciências da Computação, 5.º ano

  Informações Gerais

• Regência: J.N. Oliveira
• Departamento: Departamento de Informática
• Escola: Engenharia
• Regime: 1.º semestre
• Escolaridade semanal: 2-0-2-0

  Objectivo

Esta opção destina-se preferencialmente a alunos que tenham frequentado MFP-I e MFP-II.

Nesta opção pretende-se que os alunos tomem contacto com ferramentas que hoje existem no mercado de uso comercial e industrial, por exemplo, o Toolkit para VDM-SL da IFAD, o RAISE, o B-method etc.

Tratando-se de uma disciplina para finalistas, pretende-se desenvolver (ainda que no contexto dos Métodos Formais) um conjunto de `soft-skills' essenciais a qualquer técnico de informática dos dias de hoje. Exige-se organização e espírito cooperativo por parte dos alunos.

  Regime de Avaliação

Trata-se de uma disciplina eminentemente prática cuja avaliação é contínua (sem provas escritas) e terá em conta as seguintes componentes:

1. Capacidade de gestão de projectos de software:
   • Escolha de uma ferramenta, sua aquisição e sua instalação no Laboratório de Criptografia e Métodos Formais do Departamento de Informática.
2. Capacidade de adaptação a ferramentas novas:
   • Transporte de um trabalho de especificação formal anteriormente realizado (em MFP-II) para a ferramenta escolhida.
3. Capacidade de promoção de um produto/ferramenta:
   • Apresentação oral da ferramenta escolhida e do trabalho realizado aos colegas e alguns convidados da indústria.

  Ano Lectivo de 2006/07

Classificações à data da época especial:

Número	Aluno	Regime	Curso	Classificação	Observações
33684	António Augusto Dias de Castro Ribeiro da Silva	ORD	LMCC	F
38588	Bárbara Isabel de Sousa Vieira	ORD	LMCC	18
38164	Diogo Paulo da Fonte Lapa	ORD	LESI	16
38595	Filipe Gonçalo Gonçalves da Costa	ORD	LESI	13
38187	Flávio Miguel Xavier Ferreira	ORD	LESI	18
35821	Gonçalo Martins Gomes	ORD	LMCC	15
39846	Hélder Sérgio Alves Teixeira	ORD	LMCC	12
39442	Hugo Daniel dos Santos Macedo	ORD	LMCC	17
38204	Hugo José Pereira Pacheco	ORD	LESI	18
38220	João Rafael Ferreira Veloso	ORD	LESI	14
35839	José Manuel Serra Marques	ORD	LMCC	F
38142	José Pedro Faria e Vasconcelos Correia	ORD	LESI	18
38128	José Pedro Rodrigues Magalhães	ORD	LESI	18
35840	José Tércio Novais Soares	ORD	LMCC	F
38618	Marco António Coelho	ORD	LMCC	18
-	Martijn van Steenbergen	Erasmus	Utrecht	F
36454	Michel Ferreira Pinto	ORD	LESI	13
38209	Miguel Ângelo Pinto Marques	ORD	LESI	16
38208	Nuno Gonçalo Bettencourt da Cruz Correia	ORD	LESI	F
38153	Ricardo Araújo Carvalho Vilaça Moreira	ORD	LESI	14

Lista de projectos disponíveis:

1. Projecto: FMESoE webservice
   Supervisão: J.N. Oliveira
   Tema: O Sub-grupo para a Educação dos Formal Methods Europe tem disponível um repositório de cerca de 180 cursos de métodos formais que se pretende colocar on-line no respectivo site. Já existe um modelo formal (em VDM++) que carece de uma interface adequada (cliente web) e poderá ter que ser melhorado ou revisto. O projecto deverá incluir o refinamento deste modelo para um servidor SGDBD a escolher.
   Grupo: Marco Coelho, Bárbara Vieira, Hélder Teixeira

2. Projecto: HaCWB (Concurrency Workbench in Haskell)
   Supervisão: L.S. Barbosa
   Tema: O projecto procura desenvolver uma implementação funcional de um simulador de álgebras de processos (CCS e Pi), na linha dos conhecidos "process workbench" (eg, CWB, MWB), mas enfatizando os aspectos associados à animação interactiva. Prevê-se, nomeadamente, a inclusão de uma interface gráfica apropriada.
   Grupo: José Manuel Serra e Carlos Vilhena

3. Projecto: 2LT/Q
   Supervisão: J. Visser & A. Cunha
   Tema: In this project, you will develop a Haskell library for XML and SQL query transformation. Your library will include functions for importing XPath and SQL queries into an internal Haskell representation, for applying transformation rules to that internal representation, and for exporting the results to XPath and/or SQL again. You will demonstrate the use of your library for optimization and migration of queries.
   Grupo: Flávio Miguel Ferreira, Hugo José Pacheco

4. Projecto: 2LT/VDM
   Supervisão: J. Visser & A. Cunha
   Tema: In this project, you will create a VDM front-end for the 2LT library. The 2LT library, developed with Haskell at UMinho, supports coupled transformation of data formats and data instances, e.g. hierarchical-to-relational mappings. You front-end will import VDM-SL specifications, and translate them to internal representations of the data types of specification and of the data values in the specification. Your starting point will be the VDM-SL parser developed in the VooDooM project. You will demonstrate that through your front-end it becomes possible to perform VDM-to-relational mappings, for instance in the context of the Overture Eclipse-plugin.
   Grupo: Miguel Ângelo Marques, João Rafael Veloso, Ricardo Araújo Moreira

5. Projecto: 2LT/E ("E" for "effects")
   Supervisão: J. Visser & A. Cunha
   Tema: A two-level data transformation (2LT) consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. A typical example of a 2LT consists in transforming XML schemas into relational database schemas, coupled with the migration of the XML documents to relational tables. Recently, we have developed a type-safe Haskell library for 2LT. Meanwhile, this library was extended in order to also transform functions that manipulate the data and to handle referential constraints. These extensions where done separately and the first task of this project is to merge them into a single library. A 2LT is built by composing small refinement rules. The second task of this project is to add tracing capabilities to the library in order to know which rules have been applied in what order. The third task consists in adding non-determinism for exploring various possible transformation paths. Non-determinism will be essential to apply 2LT in the reverse direction, and the last task of the project consists precisely in applying a reverse two-level transformation to a realistic case-study. For more information on 2LT see wiki.di.uminho.pt/wiki/bin/view/PURe/2LT.
   Logistics: The project involves a 2 person group during 4 months. The group members must be good Haskell programmers and have experience with monads. The final report must be written in English.

6. Projecto: BBI (enquadramento: Projecto PortoDigital)
   Supervisão: J. Visser
   Tema: In this project, you will develop a graphical user interface for the prototype of a commercial trading engine. You will be responsible for the design of the interface, taking into account the interaction of various types of users, such as brokers, assignors, and accountants. The prototype is a Haskell application, so your user interface could be implemented with wxHaskell. Through the user interface, you will be able to give a visual demonstration of the (correct) functioning of the trading engine.
   Grupo: Gonçalo Gomes

7. Projecto: PTable
   Supervisão: A. Cunha & J.N. Oliveira
   Tema: continuação do projecto desenvolvido em MFP-II
   Grupo: José Pedro Correia, José Pedro Magalhães

8. Projecto: «Bringing Alloy, Haskell and VDM together»
   Supervisão: J.N. Oliveira & L.S. Barbosa
   Tema: Alloy é uma ferramenta para métodos formais cuja linguagem se baseia no princípio de que, num modelo de software, tudo são relações. Para mais detalhes, ver eg. a tutorial recente que se apresentou no congresso FM'06 (http://alloy.mit.edu/fm06/). O que se pretende neste projecto é investigar a base relacional de Alloy, compará-la com o uso de relações pointfree que se faz em MFP-I, MFP-II e investigar como usar o Alloy Analyzer em situações concretas, comparando-as com o que se faz com Haskell e VDM.
   Grupo: Nuno Correia

9. Projecto: Porting VDM++ source code to Overture (Eclipse)
   Proponente: P.G. Larsen (Engineering College of Aarhus)
   Supervisão: J.N. Oliveira & P.G. Larsen
   Tema: a detalhar por P.G. Larsen
   Grupo: Hugo Daniel Macedo

10. Projecto: CRM (Customer Relationship Manager) Kernel: Abordagem Open-Source
    Proponente: F.L. Neves (Sidereus SA)
    Tema: Pretende-se neste projecto construir um package 'open-source' tendo por base a especificação formal e respectiva implementação em Microsoft .NET e em Microsoft SQL Server 2000 de um componente de software intitulado 'CRM Kernel'
    Grupo: Michel Ferreira Pinto, Filipe Gonçalo Costa

11. Projecto: Graphical user interface for two-level transformation (2LT/GUI)
    Tema: A two-level data transformation (2LT) consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. A typical example of a 2LT consists in transforming XML schemas into relational database schemas, coupled with the migration of the XML documents to relational tables. Recently, we have developed a type-safe Haskell library for 2LT. In this project you will develop a Graphical User Interface (GUI) for two-level transformation. The interface should allow:
    • import of a data format, specified e.g. in XML Schema, SQL, Haskell
    • specification of rules to apply to the format, by selecting from a palette of rules and rule combinators, or by writing a high-level script
    • running the rules
    • inspecting the result and the derivation steps
    • apply the resulting data conversion function to data instances, either in backward or forward fashion
    You may want to consider using wxHakell as your GUI toolkit.
    Grupo: Diogo Lapa (em Erasmus)

  Ano Lectivo de 2005/06

Novo	Classificações: Opção V (LMCC) e Opção IV (LESI)

Lista de projectos disponíveis:

1. Tema: Especificação e Prototipagem de uma Bolsa de Valores Imobiliária
   Sumário: Pretende-se neste projecto contruir uma especificação formal e respectivo protótipo de um kernel de suporte a transacções numa bolsa de valores imobiliários.
   Proponente: F.L. Neves (Sidereus SA)
2. Tema: Especificação formal, animação e implementação da bases de dados de recursos educacionais da associação Formal Methods Europe (FME)
   Sumário: O Sub-grupo para a Educação dos Formal Methods Europe tem disponível um repositório de cerca de 180 cursos de métodos formais que se pretende colocar on-line no respectivo site. Já existe um modelo formal (em notação CAMILA) que se pretende passar para VDM++, animar nas VDMTools, melhorar e implementar num servidor SGBD a escolher.
   Proponente: J.N. Oliveira
3. Tema: CRM (Customer Relationship Manager) Kernel: Abordagem Open-Source
   Sumário: Pretende-se neste projecto construir um package 'open-source' tendo por base a especificação formal e respectiva implementação em Microsoft .NET e em Microsoft SQL Server 2000 de um componente de software intitulado 'CRM Kernel'
   Proponente: F.L. Neves (Sidereus SA)
4. Tema: Animação de Arquitecturas de Software em Haskell
   Sumário:
   • Implementação em Haskell de uma biblioteca de combinadores de componentes (cuja semântica formal está documentada em publicações do grupo) Este trabalho supõe a definição do tipo de dados "componente de software".
   • Teste da biblioteca com a montagem de um conjunto de padrões arquitecturais típicos (eg, cliente-servidor, pipe&filter, blackboard, pier-evolution, etc) e aplicação a exemplos (eg FolderFromTwoStacks, DinningPhilosophers, Ballot, etc.)
   • Integração da biblioteca na ferramenta PUReCamila (estudo preliminar)
     Contexto: Integração no projecto PURe (www.di.uminho.pt/pure)
     Supervisão: Luís S. Barbosa e Marco António Barbosa
5. Tema: PUReCAMILA: object layer
   Sumário:
   • O PUReCAMILA é um projecto que tem por objectivo re-implementar o sistema CAMILA em Haskell. Em fases anteriores do projecto foram construídos protótipos do interpretador CAMILA que incorporavam grande parte das características desse sistema (e.g. manipulação de invariantes, tratamento de erros, etc). Pretende-se, com o presente projecto, estender o PUReCAMILA no sentido de permitir a manipulação de (instâncias de) objectos CAMILA.
     Supervisão: J.C. Bacelar

  Ano Lectivo de 2003/04

Horário

2^a-feira 9h00-10h00 (T), Sala DI-0.11

3^a-feira 10h00-11h00 (T), Sala DI-0.11,

4^a-feira 11h00-13h00 (P), Sala DI-0.04.

Sumários

Brevemente disponíveis

Programa Resumido

Estudo e desenvolvimento de técnicas de análise de requisitos e experiência em interface/ coabitação de ferramentas de apoio ao uso de métodos formais (à escala industrial) com as tecnologias tradicionais. Casos de estudo - projectos propostos no contexto do Projecto PURe (FCT):

1. KF: desenvolvimento em Strafunski de um protótipo de um refinador de VDM-SL/VDM++ para SQL standard integrável nas VDMTOOLS ©.

2. PURe WP1: Especificação formal (em VDM-SL) e prototipagem (em / VDMTOOLS ©, inc. GUI) de uma «Tabela Periódica» para catálogo de algoritmos (hilomorfismos) e seu preenchimento extensivo.

Regime de Avaliação

Projecto laboratorial e sua apresentação oral pública.

Notas Finais

• À data da época de especial

  CoDisc	Nr	Reg.	Classif.	Nome
  5309V7	30171	Ord	10	Bruno Maciel Almeida Costa
  5309V7	30175	Ord	10	Bruno Pacheco Machado dos Santos
  5309V7	30235	Ord	18	Paulo Filipe Araújo da Silva
  5309V7	27685	Ord	18	Tiago Miguel Laureano Alves

  Ano Lectivo de 2002/03

Horário

• Salas: as aulas decorrem no Laboratório de Criptografia e Métodos Formais (0.0.4)
• Horário: 4^a-feira 11h-13h (P). 3^a-feira 10h-11h (T) e 17h-18h (T).

Sumários

Programa Resumido

Estudo e desenvolvimento de técnicas de análise de requisitos e experiência em interface/ coabitação de ferramentas de apoio ao uso de métodos formais (à escala industrial) com as tecnologias tradicionais. Casos de estudo - projectos propostos no contexto do Projecto EUREKA 2235 (IKF):

1. VDM-SLspecification and animation (in VDMTOOLS ©) of the IKF-CW software component repository.
   Aluno: Nuno Rodrigues [Relatório final]

2. VDM-SL specification of the IKF ontology model.
   Aluno: Marlene Azevedo [Relatório final]

3. VDM-SL specification of the Topic Map information model
   Aluno: Càndida Silva [Relatório final]

4. VDM-SL specification of the IKF Information Acquisiton Model (inc. interface between VDMTOOLS © and the Google Web APIs developer's kit)
   Aluno: Rui Castro [Relatório final]

Regime de Avaliação

Projecto laboratorial e sua apresentação oral pública.

Notas Finais

• As pautas estão ordenadas por CoDisc (código de disciplina) e Nome dos alunos.
• À data da época de recurso:

  CoDisc	Nr	Reg	Nome	Classif.
  5309V7	12613	ORD	Hugo Filipe Camelo Abreu Figueiredo	- (Faltou)
  5309V7	24874	ORD	Rui José Gonçalves de Castro	17 (dezassete)
  7009U2	25374	ORD	Marlene Azevedo da Silva	17 (dezassete)
  7009X7	28144	ORD	Cândida Susana Gonçalves da Silva	18 (dezoito)
  7009X7	9284	T-E	João Manuel Bacelar Barreto Seabra	- (Faltou)
  7009X7	25944	ORD	Miguel Pedro Eiriz Gonçalves	- (Faltou)
  7009X7	26967	ORD	Nuno Miguel Feixa Rodrigues	18 (dezoito)

  Ano Lectivo de 2001/02

Horário

• Salas: as aulas decorrem no Laboratório de Criptografia e Métodos Formais (0.0.4)
• Horário: 4^a-feira 11-13 (P). 3^a-feira 10-11 (T) e 17-18 (T).

<986>>

Sumários

Brevemente disponíveis

Programa Resumido

Estudo e desenvolvimento de técnicas de coabitação de ferramentas de apoio ao uso de métodos formais à escala industrial com tecnologias tradicionais. 'Embedding'e desenvolvimento faseado de grandes aplicações de `software'.

Casos de estudo (projectos):

1. O DTS (Data Transformation Services) é uma componente do SQL Server 2000 que proporciona o transporte de dados de uma ou mais origens (de dados) para um destino. DTS Designer é uma aplicação gráfica que permite o desenho da migração de dados entre diferentes nichos de dados. K-Migration é uma aplicação que permite a migração de dados entre base de dados, pertencente ao conjunto dos K-Line Products. Este projecto pretende desenvolver uma aplicação que tem como objectivo a tradução de um DTS Package (gerado pelo DTS Designer) para um módulo em M2L (linguagem de migração do K-Migration).

2. Uso de VDMTOOLS © em ambiente Windows/.NET. Desenvolvimento de uma especificação formal em VDM-SL do ADO.NET.

3. Projecto de utilização do método Alloy.

4. Criação de uma interface e ambiente de desenvolvimento para PICT.

Regime de Avaliação

Projecto laboratorial e sua apresentação oral pública.

Notas Finais

• À data da época especial:

CoDisc	Nr	Reg	Ano	Nome	Projecto	Classif.
5309V7	24805	ORD	5	Bruno César dos Santos Oliveira	2	17 (dezassete)
5309V7	24805	ORD	5	Mário Miguel Azevedo Cerqueira	3	17 (dezassete)
7009U2	26702	ORD	5	Avelino Alberto Vieira Pinto	1	17 (dezassete)
7009T2	20223	T-E	5	Paulo Alexandre Soares de Brito	4	Faltou
7009U2	25378	ORD	5	Óscar Rafael da Silva Ferreira Ribeiro	1	17 (dezassete)

  Ano Lectivo de 2000/01

Programa Detalhado

Estudo e desenvolvimento de técnicas de coabitação de ferramentas de apoio ao uso de métodos formais à escala industrial com tecnologias tradicionais. 'Embedding'e desenvolvimento faseado de grandes aplicações de `software'. Casos de estudo (projectos):

TEMA:

Construção de componentes reutilizáveis a partir de especificações formais.

MÉTODO:

VDM/ VDM++

FERRAMENTA:

VDMTools

TEMA:

Especificação formal e prototipagem de uma rede tipo Multibanco.

MÉTODO:

Especificação de sistemas distribuídos em Auto-Focus

FERRAMENTA:

Auto-Focus

Projectos

1. ALUNOS:

   Nuno André de Sampaio Faria, Rui Daniel Queirós Faria Gonçalves e Rui Paulo Correia Monteiro

   MÉTODO:

   VDM/ VDM++

   FERRAMENTA:

   VDMTools

   TEMA:

   Construção de componentes reutilizáveis a partir de especificações formais.

2. ALUNOS:

   Emília Dulce Teixeira de Araújo, Sandra Maria Gomes Araújo Rodrigues e Sílvia da Conceição Oliveira Freitas

   MÉTODO:

   Especificação de sistemas distribuídos em Auto-Focus

   FERRAMENTA:

   Auto-Focus

   TEMA:

   Especificação formal e prototipagem de uma rede tipo Multibanco.

Notas Finais

À data da Época de Setembro:

No CoDisc Reg Ano Nome Classif.

20217 7009T2 ORD 5 Nuno André de Sampaio Faria 16

18674 7009U2 ORD 5 Emília Dulce Teixeira de Araújo 14

21150 7009U2 T-E 5 Rui Daniel Queirós Faria Gonçalves 16

20230 7009U2 T-E 5 Rui Paulo Correia Monteiro 16

21153 7009U2 ORD 5 Sandra Maria Gomes Araújo Rodrigues 14

20239 7009U2 ORD 5 Sílvia da Conceição Oliveira Freitas 14

  Ano Lectivo de 1999/00

Programa Detalhado

• Estudo do Método-B. Antecendentes históricos (trabalhos de E.W. Dijkstra e de C.A.R Hoare). Construção de um modelo em B: variáveis de estado, invariantes e operações.
• Noção de máquina abstracta. Notação AMN (`Abstract State Notation').
• Coerência de um modelo. Provas de correcção. Ferramentas de apoio à prova de propriedades em B: o Atelier B.
• Estudo do B-toolkit. Sistema de apoio à gestão de projectos em B. Documentação em sistema de hipertexto. Cobertura do ciclo de vida. Integração com o HTML. Relatórios de erros.
• Componente laboratorial: Instalação da ferramenta. Estudo de um caso. Especificação e desenvolvimento. Apresentação e discussão oral.

Projectos

1. ALUNOS:

   Cristina Pires da Silva Cunha e Sandra Maria Miranda Fernandes

   MÉTODO:

   B-method

   FERRAMENTA:

   B-Toolkit

   TEMA:

   Especificação formal de uma biblioteca de OLAP (= `On-line analytical processing').

Notas Finais

À data da Época Normal:

No CoDisc Reg Ano Nome Classif.

21135 7009T2 ORD 5 Cristina Pires da Silva Cunha 15

20231 7009T2 ORD 5 Sandra Maria Miranda Fernandes 16

  Contacto

Para mais detalhes enviar email para qualquer dos membros do Núcleo MF do Grupo de Lógica e Métodos Formais do Departamento de Informática.

Outras disciplinas leccionadas pelo DIUM