Alunos

Número	Nome	Foto	E-mail
10934	Gonçalo Veiga		gjveiga.lesi AT gmail DOT com
13405	Manuel Costa		mane_costa AT hotmail DOT com
15141	João Bordalo		jpbordalo AT gmail DOT com
15142	André Martins		andre_batista_martins AT hotmail DOT com
15143	Luís Filipe Teixeira		filipeteixeira83 AT gmail DOT com
15220	Tiago Veloso		ti.veloso AT gmail DOT com
15260	Luís Couto		pg15260 AT alunos DOT uminho DOT pt
15330	João Martins		pg15330 AT alunos DOT uminho DOT pt
15345	Daniel Cadete		danielncadete AT gmail DOT com
15395	Nelson Gonçalves		goncalvesnelson AT gmail DOT com
15753	André Pedro		apedro DOT 1 AT gmail DOT com
15992	Inês Prada		inesprada AT gmail DOT com
15997	Mário Eiras		marioeiras AT gmail DOT com
16019	Diogo Araújo		x0z.06.araujo AT gmail DOT com
16046	Márcio Coelho		pg16046 AT alunos DOT uminho DOT pt
	João Melo		joao.silva.de.melo AT gmail DOT com

19 Jul As notas da 2ª milestone de PI1 foram (finalmente) lançadas.

12 Jul A data de entrega dos exercícios de Coq foi adiada para o dia 29 de Julho.

29 Jun - Palestra HASLab de 30-Jun foi adiada devido à ICPC'10- detalhes aqui

27 Jun - A sessão da manhã do dia 1-Jul será dedicada à preparação da última milestone - ver Sumários

27 Jun - Data da última Milestone do PI(II): 15-Julho. Mais detalhes sobre a calendarização do mês de Julho na página de Sumários

15 Jun - Actualizada informação relativa a provas de avaliação individual (ver Funcionamento)

24 Mai Atenção à data da segunda Milestone do PI(II): 17-Junho. A terceira (e última, com participação da indústria) será em meados de Julho.

22 Abr Atenção à data da primeira Milestone do PI(II): 6-Maio. A segunda será em meados de Junho e a terceira (e última) em meados de Julho.

3 Fev Atenção à calendarização das provas de avaliação e milestones (ver sumários da UCE).

9 Dez O relatório referente à primeira Milestone (10-Dez) pode ser entregue até ao dia 17-Dez.

3 Dez O fórum dos alunos encontra-se aqui.

29 Out Está a partir de hoje on-line o repositório de ferramentas da associação FME.

29 Out A sessão de CSI de 05-Nov será ocupada pelo módulo AMT (ver sumários)

29 Set As aulas começaram no dia 1 de Outubro às 9h00.

29 Set Criação do site.

Índice:

Onde

Os alunos podem deixar os seus haveres no laboratório no período de almoço. Podem ainda usar os armários que estão sob as janelas para aí deixarem material de umas sessões para outras.

A entrada no laboratório está controlada por um sistema de identificação de impressão digital, estando o acesso reservado a docentes das UCEs que aí funcionam e técnicos.

Quando

O horário de base da UCE é o seguinte:

São feitas adaptações sempre que necessário (por exemplo, aquando das milestones do Projecto Integrado (PI), sessões de docentes convidados, etc)

Regime de Avaliação

A nota final é a média pesada das notas obtidas nos diferentes módulos:

• Cálculo de Sistemas de Informação (15%).
• Análise, Modelação e Teste (15%).
• Verificação Formal de Software (15%).
• Processos e Arquitecturas de Software (15%).
• Projecto Integrado (40%).

Para obter aprovação à UCE os alunos terão que ter aprovação em todos os módulos: excepcionalmente poderão ser aprovados alunos que tenham reprovado a um dos módulos teóricos (a aprovação no projecto integrado é sempre obrigatória). Oportunamente serão indicados os métodos de avaliação para cada um dos módulos.

Classificações finais da UCE

10934 = F ; 13405 = 15 ; 15141 = 14 ; 15142 = 15 ; 15143 = 13 ; 15220 = 15 ; 15260 = 17 ; 15330 = 16 ; 15345 = 16 ; 15395 = 14 ; 15753 = 13 ; 15989 = D ; 15992 = 12 ; 15997 = 13 ; 16019 = 13 ; 16046 = 14 .

Provas de Avaliação

Notas das Provas de Avaliação Individual (18-Fev)

13405=(14,15.9);15141=(R,14.5);15142=(R,16.5);15143=(10,13.3);15220=(10,15.2);15260=(13,17.8);15330=(10,18.4);15345=(13,18.5);15395=(12,14.6);15753=(R,10.0);15992=(R,14.5);15997=(10,14.5);16019=(11,12.2);16046=(R,13.3); jm=(R,17.8).

Notas de PAS

10934= (0, 0, NA); 13405= (7.5, 6, 14); 15141= (5, 7, 13); 15142= (10, 9, 19); 15143= (6.5, 0, 8); 15220= (9.6, 6, 17); 15260= (10, 9, 19); 15330= (7.5, 7, 15); 15345= (10, 9, 19); 15395= (8, 8, 16); 15753= (3, 6, 10); 15992= (4.5, 5, 10); 15997= (8.5, 6, 15); 16019= (5.5, 6, 12); 16046= (9.6, 8, 18); jm= (0, 0, NA).

Notas de AMT (após recurso)

Notas de VFS

Para cada aluno, identificado pelo seu número, a nota de (teste,exame,ex.Coq,final).

13405 = (13.5, -, 20, 15); 15141 = (-, 9.5, 18, 11); 15142 = (-, 11.5, 18, 13); 15143 = (-, 11, 20, 13); 15220 = (11.1, -, 20, 14); 15260 = (14.1, -, 20, 16); 15330 = (-, 15.5, 20, 16); 15345 = (-, 11, 20, 13); 15395 = (-, 13.5, 18, 14); 15753 = (-, 9, 20, 11); 15989 = (-, -, 20, -); 15992 = (-, 10, 20, 12); 15997 = (-, 10.5, 20, 12); 16019 = (-, 8.5, 20, 11); 16046 = (8.6, 7.5, 20, 11).

Notas de PI(I)

10934 = F ; 13405 = 15 ; 15141 = 12 ; 15142 = 12 ; 15143 = 13 ; 15220 = 17 ; 15260 = 17 ; 15330 = 14 ; 15345 = 15 ; 15395 = 13 ; 15753 = 14 ; 15989 = 13 ; 15992 = 13 ; 15997 = 13 ; 16019 = 13 ; 16046 = 13 .

Notas de PI(II)

SIG1 = 18 ; SIG2 = 14 ; CS2 = 18 ; BSC1 = 14 ; BSC2 = 16 ; G1 = 15 ; G2 = 16.

Métodos Formais

Preâmbulo

A ciência tem a ver com o perceber-se como o mundo e as suas coisas funcionam e a tecnologia com o garantir que certas coisas que se desejam acontecem de forma fiável e repetível. A necessidade de basear a segunda em resultados da primeira é uma constante da evolução das disciplinas de engenharia, a única de facto capaz de ultrapassar as limitações do puro experimentalismo e do amadorismo, e de promover a transmissão segura do conhecimento.

Ora o resultado científico recorre, por natureza, à fórmula matemática para poder ser expresso e, assim, ser susceptível de raciocínio. É assim que as engenharias "clássicas", como a civil, a mecânica, a electrotécnica, a electrónica, etc, recorrem sistematicamente a disciplinas da matemática (algumas já centenárias) para a arrumação dos seus corpos de conhecimento. São exemplos conhecidos de todos nós o cálculo diferencial/integral, a análise numérica, a geometria analítica, etc, etc.

Com o advento das chamadas Tecnologias da Informação esta situação alterou-se. Na verdade, essas tecnologias desde cedo mostraram alguma dificuldade em sobreviver sobre tal herança científica, pelo facto de esta estar demasiado comprometida com a modelização de entidades da vida real que, como o espaço e o tempo, são por natureza contínuas e infinitas. Ora o suporte computacional capaz de mecanizar esses modelos é, por limitação física, discreto e finito. O que faz com que sejam a matemática discreta, a lógica formal, a álgebra universal, etc. as disciplinas em que o projecto científico do 'software' se alicerça.

Contudo, essas disciplinas encerram uma dificuldade - a de, por serem demasiado descritivas, os raciocínios dificilmente escalarem a problemas de tamanho real. Existem duas alternativas para sair dessa dificuldade: apostar em ferramentas de verificação (demonstradores de teoremas, etc) ou apostar em notações mais económicas e susceptíveis ao raciocínio. Este módulo segue a segunda destas vias, sendo a sua base o ensino do cálculo de relações binárias dito 'pointfree' (sem variáveis) e a sua essência a chamada transformada 'pointfree' que converte expressões da lógica e matemática discreta como forma de agilizar o raciocínios necessários.

Objectivos

Este módulo estrutura-se, pois, a dois níveis - descrição e cálculo. No primeiro, ensina-se a especificar 'software' através da criação de modelos abstractos sobre os quais se pode raciocinar e garantir propriedades desejáveis ('model-oriented specification'). Ensinam-se várias abordagens à animação e teste de modelos: o recurso à linguagem funcional Haskell (equipada com bibliotecas desenvolvidas para esse efeito), o recurso ao JML e as VDMTools (CSK) que animam o VDM-SL (ISO/IEC standard 13817-1.

No segundo, ensina-se a converter esses modelos para a notação relacional e a raciocinar sobre eles. O exercício estende-se a outras áreas da modelação como, por exemplo, a formulação de uma semântica para diagramas ER (entidade-relação), etc.

Pela sua natureza propedêutica, o módulo é central às que a acompanham neste módulo. A sua articulação com o Projecto Integrado (PI) é feita ao nível da prototipagem e animação de modelos.

Programa

• Introdução à especificação formal como método de controlo de qualidade em 'software'. Binómio modelação / implementação. Engenharia orientada ao modelo (MDE).

• Ciclo de vida do desenvolvimento formal de 'software'. Especificação formal construtiva. Modelo de um problema. Prototipagem e animação. Validação por teste. Importância da verificação formal das propriedades de um modelo. Obrigações e métodos de prova. Sub-especificação e não-determinismo. Relação (especificação) versus função (implementação).

• Introdução ao cálculo de relações. Inclusão, composição e intersecção de relações. Conversa de uma relação. Formulação de propriedades em notação "pointfree".

• Taxonomia de relações binárias. As funções vistas como casos particulares de relações. Representação de predicados lógicos por relações binárias. Ordens. Estruturação do cálculo relacional com base em conecções de Galois (CG).

• Significado de um invariante. Prova de preservação de um invariante. Noção de precondição mais fraca que garante uma propriedade. Regras para combinação de especificações que satisfazem propriedades.

• A integridade-referencial como uma classe de invariantes sobre relações simples e finitas em bases de dados. Diagramas Entidades-Relações (ERD) e sua semântica pointfree baseada na preordem de definição de relações.

• Uso do Haskell como linguagem de modelação. Invariantes, pre e pós-condições em Haskell. A biblioteca CamilaMonad. Animação de modelos em Haskell.

• Recurso ao JML para anotação formal de código Java.

• O "standard" ISO/IEC 13817-1 (VDM-SL). Significado de um modelo VDM-SL. Semântica relacional de um par pre-/post-. Relações em compreensão. Relações simples finitas e sua representação em VDM-SL ("mappings").

Bibliografia

• C. B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986.

• J.N. Oliveira. Program Design by Calculation. Draft of textbook in preparation.

Processos e Arquitecturas de Software

Este módulo constitui uma introdução ao estudo da arquitectura dos sistemas na dupla perspectiva da estrutura das suas interações e do comportamento emergente. Como os restantes módulos nesta UCE, também este adopta um ponto de vista científico-pedagógico que procura aliar o rigor e poder de cálculo matematicamente fundamentado a uma componente laboratorial que, na forma de projecto horizontal de módulo, integra aspectos metodológicos e de realização tecnológica (sobre, por exemplo, plataformas orientadas a componentes, serviços-web, linguagens de coordenação e plataformas específicas sobre e.g. Java ou C#).

A primeira parte do curso é uma introdução à especificação e cálculo do comportamento dos sistemas a partir de uma caracterização matemática das noções de interacção, como elemento base da computação, e de processo, como padrão de interações. Será colocada uma enfâse particular no estudo de processos capazes de auto-reconfigurarem dinamicamente as suas interligações e possibilidades de interação. Esta abordagem será situada no contexo da programação reactiva, onde surgiu, e do fenónomo da computação global na análise do qual é um instrumento fundamental. De um ponto de vista técnico esta primeira componente é baseada no cálculo-Pi e nos métodos coindutivos, traçando-se através deles uma ponte com o cálculo de funcionalidade e estruturas de informação discutidos noutros módulos desta UCE.

A segunda parte do curso, capitalizando nos fundamentos estudados, incide sobre a sua aplicação à especificação, análise e transformação de arquitecturas de software.

Esta segunda componente, inicia-se com uma caracterização da disciplina de arquitectura de software, referindo os standards aplicáveis e traçando a história do conceito em Engenharia de Software. Em particular será enfatizada a diferença entre arquitecturas baseadas na interconecção estática (compile-time) de módulos, orientada à macro-estrutura da aplicação e ao controlo do fluxo de recursos entre módulos, e arquitecturas baseadas na orquestração dinâmica (run-time) de componentes e serviços autónomos, distribuídos ao longo de redes de computação global e altamente heterogéneos. A ênfase é, neste último caso, colocada no controlo do fluxo de interacções (não raro baseadas em comunicação anónima e de localização variável) e na integração de entidades heterogéneas cujas ligações são estabelecidas e revistas dinamicamente, sem interrupção de serviço. Procura-se motivar os alunos para os desafios colocados pela passagem, paralela à registada na prática económica, de uma visão que enfatizava o software como produto para uma outra que o encara essencialmente como um serviço.

É nesse contexto que o curso vai caracterizar diversos estilos arquitecturais, sublinhado o modo como tanto conceitos base (e.g., objecto, contrato, interface, componente, serviço, connector, glue code, padrão, configuração, etc.) como opções metodológicas emergem dos desafios e complexidade dos problemas reais emergentes quer na concepção quer na re-engenharia de software. Discutem-se, em particular,

• arquitecturas orientadas ao objecto
• arquitecturas orientadas à componente
• arquitecturas orientadas ao serviço Em cada caso discute-se o vocabulário associado, estilos de interação, composicionalidade,

• da orquestração e interacção de componentes (objectos, serviços, recursos),
• da mobilidade e reconfiguração dinâmica dessas conecções,
• da planificação, documentação, análise e evolução arquitectural.

Programa

• Componentes, Serviços e Processos
  • Motivação: estrutura vs. comportamento; prescrição vs. observação; indução vs. coindução.
  • Interacção e cálculo de processos.
  • Componentes e Serviços como processos interactivos.
  • Mobilidade e reconfiguração dinâmica de software. Introdução ao Pi-calculus.
  • Estudo de caso e sua análise laboratorial (com recurso ao mwb).

• Projecto e Cálculo de Arquitecturas de Software
  • Motivação e história do conceito em Engenharia de Software.
  • Modelação de arquitecturas; ADL (Architecture Description Languages); Estilos e padrões arquitecturais; metodologias.
  • Arquitecturas Orientadas ao Objecto. Composição de objectos.
  • Arquitecturas Orientadas à Componente. Coordenação de componentes.
  • Arquitecturas Orientadas ao Serviço. Orquestração de serviços.
  • Documentação, projecto e análise de arquitecturas de software.
  • Estudos de caso.

Projecto Integrado (II)

15-July Milestone

Workshop schedule

Morning:

Afternoon:

Workshop Skype id: uminho-di-a1

Projectos selecionados

Constituição dos grupos:

Projecto Integrado (I)

Grupos

Milestone 1

• Objectivos:
  • Especificar em Alloy um problema de média dimensão.

• Deadline:
  • 10 de Dezembro de 2009.

• Deliverables:
  • Modelo Alloy.
  • Versão preliminar do relatório a entregar na Milestone 2 (com 10 páginas no máximo).
  • Apresentação de 20m no dia 10 de Dezembro de 2009.

Milestone 2

• Objectivos:
  • Implementar um protótipo em Java do sistema modelado na Milestone 1.
  • Anotar o código com invariantes, pré- e pós-condições em JML.
  • Efectuar teste do código por forma a atingir uma cobertura aceitável.

• Deadline:
  • 25 de Fevereiro de 2010.

• Deliverables:
  • Código Java+JML com os respectivos testes.
  • Relatório do trabalho desenvolvido no 1º semestre (com 20 páginas no máximo).
  • Apresentação de 20m no dia 25 de Fevereiro de 2010.

Relatórios

Os relatórios deverão seguir o formato seguinte:

\documentclass[a4paper]{article}

\usepackage[portuges]{babel}
\usepackage[latin1]{inputenc}
\usepackage{a4wide}

\begin{document}

\end{document}

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.avisos { color: #444; font-size:12px; }

.natWebTitle { font-size:25px; }

.natMainFooterContents, .natMainHeaderContents { padding:0px; margin:0px 0px; }

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.

Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:

three spaces * [ webname . ] wikiName - SMTP mail address
three spaces * [ webName . ] wikiName
three spaces * SMTP mail address
three spaces * SMTP mail address : topics
three spaces * [ webname . ] wikiName : topics

In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:

• Specify topics without a Web. prefix
• Topics must exist in this web.
• Topics may be specified using * wildcards
• Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
• Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
• Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.

For example: Subscribe Daisy to all changes to topics in this web.

   * daisy.cutter@flowers.com

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.

Tip: List names in alphabetical order to make it easier to find the names.

Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.

Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.

Related topics: WebChangesAlert, TWikiUsers, TWikiRegistration

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Education/MFES0910 Web