Arquitectura e Cálculo

Funcionamento

Docentes

• José Proença
• José Nuno Oliveira

Método de avaliação

• Teste individual escrito (60%) + 3 trabalhos (40%)
  • Prazo de entrega do trabalho 2: 31 Maio 15 Junho @ 23:59
  • Apresentação do trabalho 2: 1 Junho 16 Junho - 10 min por grupo
  • Prazo de entrega do trabalho 3: 22 Junho @ 23:59
  • Teste individual com consulta: 8 Junho
  • Exame com consulta: 29 Junho @ 9:00

Atendimento

• Horário: 4ª 10h-12h (por marcação)
• Marcação: jose at proenca dot org

Objectivos

Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos.

Programa Resumido

• Introdução aos sistemas reactivos
• Fundamentos
• Modelação e análise de sistemas reactivos
• Arquitectura de sistemas reactivos
• Projecto e integração de ferramentas.

Material de apoio

Slides

• 0 - Introduction
• 1 - Revisions
• 2 - Labelled Transition Systems
• 3 - Modal Logic
• 4 - Real Time Systems - modelling
• 5 - Real Time Systems - verification
• 6 - Coordination perspective - introduction
• 7 - Reo - semantics - até ao slide 40
• 8 - Reo - extra - não foi dada
• 9 - Software Components as Monadic Mealy Machines (MMM) - versão de 25-Mai.

Material

• Tutorial - rope-bridge in mCRL2
• Assignment 1 - a mCRL2 exercise
• Assignment 2 - Time and Reo coordination
• Teste do ano anterior (2015-2016)

Software

• Bibliotecas em Haskell (última actualização: 24-Mai)

Links úteis

• mCRL2 website
• UPPAAL website
• Reo website

Bibliografia

• Formal Modeling and Analysis of Software Architecture: Components, Connectors, and Events (pdf)
• Principles Of Model Checking (pdf)
• Modal Logic for Open Minds (pdf)
• Modal Logic: a semantic perspective (pdf)
• Reactive Systems: Modelling, Specification and Verification (pdf)
• A tutorial on Uppaal (pdf)
• Overview of Thirty Semantic Formalisms for Reo (pdf)
• Reo + mCRL2 : A framework for model-checking dataflow in service compositions (pdf)

Resultados de aprendizagem

• Conhecer e caracterizar modelos para computação reactiva baseados em diferentes tipos de sistemas de transição, nomeadamente com evolução não-determinística, em tempo real ou estocástica.
• Formular propriedades sobre esses modelos e analisar a sua satisfação.
• Familiarizar-se com a noção de coordenação de software e utilizá-la produtivamente na definição de arquitecturas de sistemas reactivos.
• Conhecer e utilizar ferramentas computacionais de suporte.
• Integrar os conhecimentos adquiridos para utilização no projecto de engenharia de sistemas reactivos.

Alunos - pautas provisórias

[ Acesso às edições anteriores de 2014-15 e 2015-16 ]

-- Página criada por LuisSoaresBarbosa - 28 Sep 2016

15 Jul - Exames da época especial: ver Sumários.

22 Jun Notas dos testes e do TP2 já sairam - A&C.

06 Jun Nova data para apresentações dos trabalhos - 20 Junho, ver Sumários.

24 Mai Datas para entrega e apresentações dos trabalhos adiada - para 15 e 16 Junho, respectivamente.

9 Mai Anunciadas datas para as apresentações dos trabalhos (1 Junho) e para o teste (8 Junho).

9 Mai Disponíveis os slides mostrados até ao momento no último módulo de A&C.

25 Abr Entrega do trabalho prático (UPPAAL) adiado para 3 Maio @ 23:59.

6 Abr Notas do trabalho prático 1 já estão disponíveis - A&C.

20 Mar Trabalho prático 1: entregar até dia 23 Março; Trabalho prático 2: disponível em Material - A&C.

24 Fev - Primeiro trabalho prático já saiu, em "Material" de A&C.

14 Fev - Ver Material em A&C.

10 Fev - Lançadas a classificações finais de E&M.

10 Fev - Importante: as aulas das disciplinas do perfil de MFES passam, a partir da próxima semana (inclusive), para a sala DI 1.08.

6 Fev - WS de apresentação de temas MFES/LEI: ver Sumários.

6 Fev - Apresentações dos trabalhos: ver Sumários. Cada apresentação não pode demorar mais que 20 min, discussão incluída. No caso de desejarem apresentar slides devem enviá-los para o responsável da disciplina no dia anterior.

28 Jan - Trabalho de E&M: a data de entrega passou para 3-Fev até às 12h.

21 Jan - Enunciado do teste de E&M disponível, com correcção de algumas perguntas.

15 Jan - Estão disponíveis duas bolsas para desenvolver trabalho no projeto Green Software Laboratory GSL. Se tens licenciatura (ou os 3 primeiros anos do mestrado) completos concorre! Mais informações aqui.

06 Dez - E&M, T+TP suplementar de amanhã: por falta de salas a aula só poderá ser às 16h00, na sala 1.09, ver Sumários.

30 Nov - E&M: já está disponível o enunciado do TP.

29 Nov - ATS, aula extra esta 4a feira, dia 30/11 às 14:00.

29 Nov - E&M, grupos de trabalho: os alunos que ainda o não fizeram devem enviar ao responsável da disciplina a constituição do seu grupo (de dois alunos cada). O TP será anunciado amanhã, 30-Nov.

20 Nov - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides (PDF) até ao 115; fazer os exercícios 37, 40, 46 e 47.

3 Nov - Está disponível uma bolsa para desenvolver trabalho na plataforma Alloy4Fun. Se tens licenciatura (ou os 3 primeiros anos do mestrado) completos concorre! Mais informações aqui.

13 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 97; fazer os exercícios 32, 33, 34.

3 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 79; fazer os exercícios 25, 28, 30, 31.

29 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 65; fazer os exercícios 20, 22, 25-26.

14 Out - E&M, preparação em casa para a próxima aula ('Flipped Classroom'): ler slides até ao 45; fazer os exercícios 7 a 10.

6 Out - O teste de ATS será no dia 5 de Janeiro e o teste de E&M será no dia 12 de Janeiro.

20 Set - As aulas das disciplinas do primeiro semestre iniciam-se a 22-Set.

Especificação e Modelação

Classificações do exame da época especial:

a64287 = R; pg22842 = R.

Classificações finais:

a32652 = 10; a53791 = 10; a64287 = R; a64365 = R; a67652 = F; a67709 = 10; a70058 = F; a70430 = 14; a70441 = 10; a70644 = F; a71580 = 13; a71625 = F; a72204 = 11; a72205 = R; a72227 = 11; a72424 = 14; pg22842 = F; pg31577 = 10; pg32996 = R.

Método de avaliação

• Teste individual escrito (70%, ≥ 8)
• Trabalho de grupo (30%, ≥ 10)
• Presença obrigatória nas aulas

Enunciados de provas escritas de avaliação (T)

Data	Descrição	Ficheiro
12-Jan-2017	Teste	PDF (com a correcção de algumas perguntas)
26-Jan-2017	Exame de recurso	PDF

Enunciado do Trabalho (TP)

Introdução - Nesta disciplina foram estudados métodos de especificação, modelação e raciocínio para a produção de software de alta fiabilidade. Todos os sistemas de segurança-crítica exigem software fiável, por exemplo nos equipamentos médicos, nos transportes aéreos, etc. A norma de certificação DO-178B é uma diretriz sobre segurança do software crítico destinado à aviação.

O artigo Modelling an Aircraft Landing System in Event-B, que descreve a modelação formal de um sistema de controlo do trem de aterragem de um avião baseado nos requisitos impostos pela Federal Aviation Administration dos EUA, é o ponto de partida para este trabalho.

O que é para fazer - os grupos de trabalho devem estudar o artigo acima referido com atenção por forma a perceberem bem qual é o problema que é abordado. Ao mesmo tempo, deverão informar-se sobre a linguagem de modelação Event-B, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é exprimir o mesmo modelo em Alloy, de forma o mais simples possível. Note-se que não se pretende uma tradução à letra do modelo dado, mas antes um modelo independente e simplificado. Mais do que a quantidade, valorizar-se-á a qualidade e a capacidade de abstracção.

Prazos e "deliverables" - os grupos deveram entregar, até à data limite de 31-Jan-2017, um pequeno relatório (em inglês) onde conste o código Alloy que desenvolveram. Deverão também preparar uma apresentação do seu trabalho (slides) prevista para (no máximo) 10 minutos. As orais destas apresentações decorrerão de 1 a 10 de Fevereiro.

Os alunos deverão estar atentos a esta página quanto a prováveis esclarecimentos sobre este trabalho que os inicia na aplicação de métodos formais a problemas reais. Bom trabalho!

Material pedagógico

• Modeling, Specification, and Verification: slides introdutórios.
• Exercícios sobre SMV: as questões marcadas com CTL requerem conhecimento sobre lógica temporal CTL que ainda não foi leccionada este ano.
• Exemplos SMV: barqueiro, cadeira pesada, algoritmo de exclusão mútua de Peterson (sem módulos e com módulos).
• A perspective on Model Checking. Estes slides sobre model checking abarcam muito mais matéria do que a que será leccionada este ano, mas podem ser úteis para quem desejar saber mais sobre este assunto (ver bibliografia no final). Em particular, este ano usamos SMV e não Petri Nets como linguagem de modelação.
• J.N. Oliveira. Specification and modelling: where everything becomes a relation (versão de 20-Nov-16, 130 slides).

Bibliografia

• D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

• C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)

Ferramentas

• Alloy
• NuSMV

Exemplos / bibliotecas Alloy

• Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.

• Eu sou o meu próprio avô (avo.als e avo.thm).

Desafios Alloy

• Barqueiro
• Unidades Curriculares de Especialização
• Agenda telefónica
• Leilões

Alunos

Nome	P/C	Nr	Curso	Grupo	Fot
Axel da Silva Ferreira	C	a53064	MiEI	G4
Daniel Gonçalves Rodrigues	C	a67634	MiEI	G9
Daniel da Fonte Torres	EC	a70058	LCC	G8
David António Cardoso Moreira	P	a64287	MiEI	G2
David Miguel Duarte Rodrigues Alves	C	a53791	MiEI	(cong)
Diana Filipa Oliveira	C	a67652	MiEI	G7
Diogo Filipe da Silva Vilaça	P	a72227	MiEI	G3
Fernanda Raquel Cerdeira Alves	C	a64365	MiEI	G2
Fátima Cristiana da Costa Conceição	P	pg22842	MMC	(cong)
Gil Gonçalves	C	a67738	MiEI	G7
Hugo Filipe da Silva Ribeiro	P	pg32996	MEI	G5
Isac Pereira Oliveira Meira	P	pg31577	MEI	G8
José Nuno Castro de Macedo	P	a72424	MiEI	G3
José Paulo Queiroga Amorim Fernandes	P	a72204	MiEI	G6
João Bernardo Machado Quintas Dias da Costa	P	a70430	MiEI	G1
João Luís Braga Simões Romero	C	pg31384	MEI	G5
Luís Martinho de Aragão Rego da Silva	C	a72205	MiEI	G9
Mário Jorge Viana Ferreira	P	a70441	MiEI	G6
Nelson Arieira Parente	C	a71625	MiEI
Nuno Alberto Pires Fernandes	C	a61066	MiEI	G4
Pedro Duarte Cardoso Lopes	C	a32652	MiEI	(cong)
Rafael Alexandre Antunes Barbosa	P	a71580	MiEI	G1
Ruben Miguel Cunha Santos	C	a70644	MiEI
Saulo Rodrigues e Silva	?	id5541	PDINF
Sandra Isabel Lopes Ferreira	P	a67709	MiEI	(cong)

Atendimento electrónico (FAQs)

(Esta secção será actualizada regularmente com as dúvidas mais frequentes que forem colocadas à equipa docente.)

• Q1 - Tenho dificuldade em decorar a diferença entre núcleo e imagem de uma relação. Há alguma mnemónica que possa ajudar?

Cohesive Project (Laboratório de Engenharia Informática)

The main aim of this course unit (10 ECTS) is for students to engage in group work around a project proposed by industrial or R&D partners.

Students thus have the opportunity to apply the theoretical background of the other MFES modules to real problems, bridging their background with industry and research problems.

Groups will have an external adviser from the partner proposing their theme and a local tutor.

Interesting and useful slides for preparing your milestone presentations:

• http://research.microsoft.com/en-us/um/people/simonpj/papers/giving-a-talk/writing-a-paper-slides.pdf

List of Projects

Brochure of project themes: PDF

Start-up Workshop

The start-up MFES workshop will take place on Feb 9th, between 10h-13h, with the following schedule:

10h00 - Welcome
10h15 - ASML (NL) - André Passos	(Slides)
10h35 - ESA (NL) - Tiago Jorge
10h55 - BOSCH (PT) - J.A. Saraiva
11H15 - Break
12h00 - INTO-CPS (IR) - L. Couto
12h20 - OU (NL) - Stef Joosten	(Slides)
12h40 - Closing

Milestones

Dates TBA

Students of the MFES specialization

(List to be confirmed.)

-- JoseNunoOliveira - 21 Jan 2017

.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/MFES1617 Web