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

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

[ Contacto | Informações Gerais | Objectivo | Regime de Avaliação | Cursos
tinynew.gif2006/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

  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

tinynew.gifClassificaçõ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

  Ano Lectivo de 2002/03

Horário

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

  Ano Lectivo de 2001/02

Horário

<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

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):

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:

NoCoDiscRegAnoNomeClassif.
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

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:

NoCoDiscRegAnoNomeClassif.
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


J. Nuno Oliveira 2007-10-13