AVISO (31/1): Final do torneio do CodeDefender?Live: foto.
AVISO (27/1): A final do torneio do CodeDefender? é 6a feira, dia 31/1 às 15:00 (no Aquário do piso 2 do DI).
AVISO (23/1): O exame é dia 28/1 às 9am (sala CP1-1.10).
- Nesse dia de tarde (14:00-16:00, sala de reuniões do DI) daremos um tutorial sobre Selenium (teste de applicações web), no contexto do programa doutoral MAPi: os alunos de ATS estão convidados a assistir.
- Ás 16:00 tentaremos fazer a final do torneio CodeDefender? (a confirmar com os finalistas).
- Até ao fim do dia 27/1 os alunos deverão enviar num ficheiro zip com o trabalho (todo o código) + relatório + slides para ats.2019.2020@gmail.com
AVISO (21/1): A apresentação do trabalho e torneio é na sala DI-1.09.
AVISO (17/1): O horário da apresentação dos projetos e do torneio pode ser consultado no link:
Apresentação + Torneio
- Quem não tiver grupo (ver secção Grupos) deve enviar email para os docentes (há dois grupos de reserva).
- Os grupo podem trocar de horário de apresentação/torneio desde que ambos grupos concordem.
- Na apresentação todos os membros do grupo devem estar presentes.
- Os grupos devem entregar o relatório impresso.
AVISO (15/1): As notas do teste estão disponíveis na secção da availação.
O teste pode ser consultado, 2a feira, dia 20/1, às 10am (no gabinete DI:2.09)
O torneio CodeDefender? será realizado em simultâneo com as apresentações do projeto.
AVISO (13/1): A entrega e apresentação do projeto será realizada no 3a feira, dia 21 de Janeiro.
A apresentação consiste em duas partes: Na 1a parte os grupos devem preparar uma pequena apresentação (10 minutos) onde devem descrever o que fizeram e os resultados atingidos. A 2a parte consiste numa "tool demo" da aplicação desenvolvida, que deverá também ser preparada com cuidado. No total a apresentação é de 30 mintos.
Em breve será definida o horário de apresentação de cada um dos grupos.
As notas do teste serão aqui disponibilizadas esta 4a feira.
Equipa Docente
João Saraiva: aula teóricas
José Nuno Macedo: aulas laboratoriais
Aula 0 (17/09): Apresentação da disciplina.
Aula 1 (01/10): (T + PL) Combinadores de Parsing. "Embedded Domain Specific Languages". Gramáticas (BNF) como uma EDSL em Haskell: Combinadores de Parsing.
Aula 2 (08/10): (T + PL) Semântica Estática de Linguagens de Programação: Análise de Nomes.
Aula 3 (15/10): (T + PL) Software Metrics e Code Smells. O sistema SonarQube.
Aula 4 (22/10):
T: Software Refactoring: Introdução e Apresentação do catálogo de Java. Software "Technical Debt".
TP: Aplicação de Refactorings disponíveis no IntelliJ? a software Java.
Aula 5 (29/10):
T: Análise de Consumo de Energia: Introdução a Green Software.
TP: Apresentação da framework RAPL para monitorizar o consumo de energia. Resolução de Exercícios.
Aula 6 (05/11):
T: Teste de Sofware: Introdução. Cobertura de Testes.
TP: Apresentação da framework de teste unitário JUnit (e HUnit). Resolução de Exercícios.
Aula 7 (12/11):
T: Geração Automática de Casos de Teste.
TP: Apresentação do sistema QuickCheck? . Resolução de Exercícios.
Aula 8 (19/11):
T: Geração Automática de Casos de Teste: Continuação.
TP: Apresentação do sistema EvoSuite? . Resolução de Exercícios.
Aula 9 (26/11): T: Teste de Propriedades.
TP: Resolução de Exercícios em QuickCheck?Aula 10 (03/12): T: Análise da Qualidade dos Testes via Mutações.
TP: O sistema de mutação de testes PIT. Resolução de exercícios.
Aula 11 (10/12): T: Localização de Falhas. Correção Automática de Programas TP: Teste de aplicações Web: A framework Selenium. "Gamefication" da tarefa de Teste de Software: Competição entre os grupos de projeto.
Aula 12 (17/12): T + TP: Teste Individual.
Fichas de Exercícios
Ficha 1: Combinadores de Parsing
*Parsing.pdf*
Ficha 2: Static Semantics
*Semantics.pdf*
Ficha 3: Refactoring
Refactoring.pdf
Ficha 4: Unit Testing & Cobertura
*Testing.Cobertura.pdf*
Ficha 5: Geração de Casos de Teste em QuickCheck?Geração de Valores.pdf
Ficha 6: Geração de Testes Unitários em EvoSuite?EvoSuite.pdf
Ficha 7: Teste de Propriedades em QuickCheck?property_testing.pdfFicha 8: Mutação de Testes Mutation-Testing.pdfEntrega da Geração Automática de Logs: A solução da geração automática de inputs para a aplicação UmCarroJa? ! deve ser entregue enviando a solução para o seguinte email: ats.2019.2020@gmail.com
O email deve ter o título: Entrega - Logs da UmCarroJa? ! e incluir o nome dos elementos do grupo. Em anexo deve ser incluído um ficheiro zip com todo o código da solução. Deve ainda ser incluído um ficheiro readme.txt onde se descreve como executar o software.
Data Limite: 04 de Dezembro (PT time)
Software
1- Combinadores de Parsing: Biblioteca desenvolvida na aula: *Parser.hs*Exemplo desenvolvido na aula:Lang.hs2-Projeto UMCarroJa?(desenvolvido pelos alunos na dsciplina de POO): enunciado.pdfSoluções dos alunos: p1.zip e
p2.zip3-Projetos Java: Poligono (Poligono.zip) e Contactos (Contactos.zip)
4-Monitorização do Consumo de Energia:Rapl.tar.gz
Projeto em Grupo
O enúnciado do projeto a desenvolver em grupo está disponível aqui(versão atualizada em 19/11)Ficheiro de Log para execução em batch:logsPOO_carregamentoInicial.bak
Regime de Avaliação
A avaliação consiste em três componentes: prova individual (PI) (teste ou exame escritos), Projeto em Grupo (PG) (a resolver durante o semestre) e Avaliação Contínua (AC) (com base em problemas propostos nas aulas TP). As provas escritas são de consulta de material impresso, apenas.
A Nota final é calcula de acordo com a seguinte fórmula: 40% PI + 40% PG + 20% AC, com nota mínima de 8 valores em todas as componentes de avaliação.
O teste individual é de consulta: os alunos podem consultar todo o material (não eletrónico) que tiverem consigo.
Datas da Avaliação
Prova Individual:: 17/12/2019(última aula de 2019)Exame:: 28/01/2020(a confirmar)Entrega do Projeto em Grupo:14/01/2020(a confirmar)
17 Set - Vídeo de apresentação da edição de 2020/21.
30 Mar - VF: alteração do método de avaliação. 21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.
10 Fev - CSI: afixadas as notas finais na página de CSI.
4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.
28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.
26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.
13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.
13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.
13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.
13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.
5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.
2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.
3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.
24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.
12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.
10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.
29 Out - CSI: Formulário actualizado colocado na página respectiva.
2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.
26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).
17 Set - Início das aulas: 17-Set (ATS).
-- JoseNunoOliveira - 17 Sep 2019
Métodos formais e qualidade de software. Conceitos básicos: modelo, especificação, verificação e prova.
As relações binárias polimórficas como linguagem de especificação formal universal. Setas e diagramas. Estudo do cálculo relacional 'pointfree'. Conexões de Galois. Polimorfismo paramétrico.
O papel das funções na taxonomia das relações binárias. Teorema grátis de uma função polimórfica.
Atributos e dependências funcionais. O modelo de dados 'pares valores-chave' construído com relações simples, emparelhamentos e coprodutos. Integridade referencial.
Preservação de invariantes e satisfação. Cálculo da precondição mais fraca 'wp (f, p)' para uma dada função 'f' e invariante 'p'. Relações (invariantes) como tipos.
'Design by contract' por cálculo apoiado por model-checking.
Breve estudo da interpretação abstracta. Funções invariantes. Simulação relacional. Propriedades de segurança e de animação. Redução do espaço de estados por interpretação abstrata.
Formal methods for software quality. Basic concepts: model, specification, verification and proof.
Polymorphically typed binary relations as a universal formal specification language. Arrows and diagrams. Binary relations in Alloy. Study of the pointfree relational calculus. Galois connections. Parametricity.
The role of functions in the taxonomy of binary relations. Relations as types, inc. data type invariants. Theorems for free.
Attributes and functional dependencies. Key-value-pair data model = relational simplicity + pairing + coproducts. Referential integrity.
Data type invariants: preservation and satisfiability. Calculation of weakest preconditions for invariant preservation.
'Design by contract': combining model-checking with algebraic calculation. Refinement ordering on relations.
Brief study of abstract interpretation. Invariant functions. Relational simulation. Safety and liveness properties relationally. Reducing the state space by abstract interpretation.
Duas provas de avaliação (mini-teste + teste) e exame de recurso.
Avaliação contínua com base em problemas dados nas aulas TP.
As provas escritas são de consulta de material impresso, apenas.
O mini-teste é eliminatório de matéria para o teste e vale 50%.
Bibliografia
J.N. Oliveira. Program Design by Calculation (, 1.9Mb), Departamento de Informática, Universidade do Minho. Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta disciplina no corrente ano lectivo são o quinto, o sexto e o sétimo.
Formulário CSI: ( 137K) - Leis do cálculo relacional básico.
Caso de estudo: ( 127K) - Especificação relacional do calendário de um campeonato de futebol (e sua conversão para Alloy).
Caso de estudo: ( 52K) - Especificação relacional do problema da 'merceraria da D. Acácia' (com modelo Alloy).
Script alloy.sed para converter instâncias geradas pelo Alloy para Haskell - em Alloy, visualizar instância em modo Txt e copiar para ficheiro, eg. i.txt; de seguida fazer, numa shell, sed -f alloy.sed i.txt
Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.
Módulo Alloy: prod.als - produtos cartesianos em Alloy.
Biblioteca Haskell: RelCalc.hs - Cálculo relacional básico em Haskell (precisa da biblioteca Cp).
Q01 - Como é que se deve abordar o exercício 5.22? Parece muito trabalhoso...R: O que se pede é provar que a composição preserva os 4 critérios principais (injectividade, sobrejectividade, etc). Mas basta provar que preserva a injectividade e sobrejectividade apenas, pois os outros casos derivam desses por (5.34) e (5.35). Vejamos como provar que a composição preserva a injectividade (NB: completar / estudar as justificações). São dadas R e S injectivas:
(R . S ) é injectiva
<=> { definição }
ker (R . S ) ⊆ id
<=> { def kernel }
ker ( S◦ . R◦ . R . S ) ⊆ id
<= { R injectiva (R◦ . R ⊆ id) por hipótese; regra do ponto-médio B }
ker ( S◦ . S ) ⊆ id
<= { S injectiva (S◦ . S ⊆ id) por hipótese; regra do ponto-médio B }
id ⊆ id
<= { trivial }
true
Q02 - Consigo ver que o exercício 5.21 deverá basear-se nas leis (5.62) e (5.63) mas não consigo completar o raciocínio. Como devo prosseguir?R: Ou S vai ser simples e R injectiva ou vice-versa. Coloquemos a primeira hipótese:
(P ∩ Q)·S = (P·S) ∩ (Q·S)
<= { (5.62) }
P · img S ⊆ P ∨ Q · img S ⊆ Q
<= { img S ⊆ id por hipótese; regra do ponto-médio B }
P · id ⊆ P ∨ S · id ⊆ S
<= { P · id = P etc }
true
Agora é só verificar R·(P∩Q) = (R·P)∩(R·Q) para R injectiva, seguindo o mesmo método.
Q03 - Na resolução da questão 4 do teste do ano passado há uma altura em que chego a qualquer coisa como dE . V . i1◦ ⊆ Di . i1◦. Por monotonia da composição (. i1◦) consigo ver que dE . V ⊆ Di implica dE . V . i1◦ ⊆ Di . i1◦. Mas eu preciso que sejam equivalentes. Sugestões?R: Por 'shunting' de i1◦ do termo inferior para o superior (sem o converso), obtém-se i1◦ . i1 nesse lado. Ora i1◦ . i1 = id pois i1 (e i2) são injecções (funções injectivas, cujo núcleo é id). Basta então 'cortar' i1◦ . i1, não havendo perda da equivalência.
Q04 - Não sei como pegar no exercício 5.24...R: Este tipo de exercícios deve ser abordado usando monotonia ou regras de algibeira como (5.82, 5.83) etc. Exemplo: sabemos que R ∩ S ⊆ R fazendo X := R ∩ S na propriedade (5.58) e simplificando. Vamos supor que R é simples. Como "menor que simples é sempre simples" (5.82) então R ∩ S será simples. Etc para os outros casos.
Q05 - Como é que se aplica a igualdade indirecta no exercício 5.46? Não consigo ver como.R: A igualdade c◦ · (⊤ − c) = ⊥ é equivalente a c◦ ·(⊤−c) ⊆ ⊥. Por (5.151) podemos subir o lado inferior, para c◦ ·(c⇒⊥) ⊆ ⊥. A partir daí aplica-se a (5.154), obtendo-se (c◦ ·c⇒⊥) ⊆ ⊥. Agora é que se pode aplicar a igualdade indirecta para mostrar que c◦ ·c⇒⊥ = ⊥.
Q06 - Não estou a conseguir fazer a primeira prova do exercício 5.37. Como é que se pega na questão?R: Ora vejamos:
[R,S]·[T,U]◦
= { (5.117) }
(R·i1◦ ∪ S·i2◦) · [T,U]◦
= { justificar }
(R·i1◦·[T,U]◦) ∪ (S·i2◦·[T,U]◦)
= { justificar }
R·([T,U]·i1)◦ ∪ S·([T,U]·i2)◦
.... (Agora é só continuar)
Q07 - Ao resolver uns exercícios deparei-me com uma dúvida: R◦ × S◦ = (R × S)◦ verifica-se?R: Sim, verifica-se, como facilmente se prova: ( R × S )◦ = ⟨R·π1,S·π2⟩◦ = (π1◦ · R·π1 ∩ π2◦ · S·π2)◦ = R◦ × S◦
Q08 - Consegui resolver a primeira prova do 5.39 mas não estou a conseguir resolver a segunda...R: Na segunda usam-se as propriedades dos coprodutos. Por exemplo, se se começar por (g+k)◦ . (f + h), como (f + h) = [ i1.f, i2.h],
usa-se fusão-+ (relacional, igual à funcional) e fica-se com [(g◦+k◦).i1.f,(g◦+k◦).i2.h] (onde também se usou 5.123). De seguida obtém-se [i1.g◦.f,i2.k◦.h], que é igual a f/g + h/k.
Q09 - No teste, para quem realizar a 2ª parte da matéria, excluindo a matéria do mini-teste, que capítulos sairão?R: A matéria que foi dada depois do miniteste é a seguinte: secções 5.20, 5.21, 5.24 e capítulo 7.
Q10 - Não consigo perceber a justificação ao fundo da página 255.R: É de esperar, já que a justificação está muito imprecisa. Em geral, as funções constantes são tudo menos injectivas (!). Mas, aqui, o tipo de const c é 1 -> N0 (vejam porquê). Logo, const c é injectiva, pois o seu núcleo é de tipo 1 -> 1 e a maior relação possível nesse tipo é id : 1->1. (Agradeço esta dúvida, pois permitiu melhorar já a justificação que irá sair na próxima versão dos apontamentos.)
Q11 - Na última questão do teste de 17/18 não consigo justificar o terceiro e o quarto passo.R: As justificações são as seguintes: 3) teorema grátis de swap; 4) (F8), após fazer-se 'shunting' de θº.
Q12 - Na questão 6 do teste do ano passado não consigo justificar o segundo passo.R: Fazendo 'shunting' de splitAt da esquerda para a direita em splitAt ⊆ ((R* × R*) ← R*) · splitAt ficamos com id ⊆ splitAtº .((R* × R*) ← R*) · splitAt. De seguida introduzimos variáveis, eg. n e n'. Como n id n' é n=n', uma dessas variáveis desaparece.
Q13 - Não sei como justificar o penúltimo passo da questão 7 (segunda parte) do teste de 17/18.R: Dos quatro termos que estão a ser reunidos, se se isolar i1·(R◦·R)·i1◦ ∪ i2·(S·S)·i2◦, verifica-se que essa reunião é ker R + ker S por aplicação das leis dos coprodutos (R+S = [ i1· R, i2· S ] etc).
Q14 - Não percebo qual a razão para a cláusula 'injective(const e· (const c)◦)' desaparecer no penúltimo passo da prova sugerida para a questão 7 do teste de 18/19.R: Uma relação R é injectiva sse ker R ⊆ id. Neste caso, R = const e· (const c)◦, logo ker R = const c . (const e)◦ . const e· (const c)◦ ⊆ id. Se fizermos os 'shuntings' do costume, obtém-se ker R ⊆ id ≡ ⊤ ⊆ ⊤, por (6.28).
Links
History of Formal Methods - links referidos na primeira aula teórica:
Os carros modernos oferecem várias funcionalidades de segurança e conforto baseadas em componentes de software. Em particular, são já comuns atualmente sistemas de luzes exteriores adaptativos e de controlo de velocidade. Estes sistemas recolhem informação tanto de sensores (e.g., de luminosidade ou de velocidade) e da interface com o condutor (e.g., botões ou opções no computador de bordo), que é depois usada para controlar os atuadores (e.g., luzes externas ou os travões). É também comum que estes sistemas sejam adaptáveis para diferentes mercados (e.g., carros vendidos na UE ou nos EUA têm que seguir diferentes regras). O seguinte apontador descreve possíveis requisitos para sistemas deste tipo, e foi lançado como desafio numa conferência sobre métodos formais como os que estudamos nesta UC. Disponibiliza também um conjunto de sequências de validação que exemplificam possíveis execuções do sistema.
Os grupos de trabalho devem estudar o documento de referência referido acima com atenção, por forma a perceberem bem qual é o problema que é abordado. Naturalmente, devido à natureza das ferramentas, aspetos contínuos como o tempo real e a velocidade terão que ser abstraídos. Não é também expectável que cada grupo modele todas as componentes do sistema, ficando à consideração de cada um que aspetos focar. O modelo deve no entanto ser suficientemente rico em estrutura e comportamento, e permitir a verificação de alguns dos requisitos. Algumas sugestões são:
Focar-se apenas num sistema (e.g., o de luzes exteriores)
Focar-se apenas numa das funcionalidade do sistema (e.g., luzes de direção)
Focar-se apenas numa configuração concreta (e.g., mercado EU)
Trabalho 1 sobre Alloy/Electrum
O objetivo deste trabalho é desenvolver um modelo Electrum de (uma parte) deste sistema, assim como um theme que facilite a compreensão das instâncias. Os grupos deverão entregar por email o trabalho até à data limite de 4-Dec-2019 (um modelo Electrum, devidamente comentado, e o respetivo theme).
Trabalho 2 sobre SMV/TLA+
O objetivo deste trabalho é desenvolver um modelo em SMV ou TLA+ de (uma parte) deste sistema. Os grupos deverão entregar por email o trabalho até à data limite de 15-Jan-2020 (um modelo SMV ou TLA+, devidamente comentado).
Project ideas from Prover Technology (if you are interested in any of these projects please contact Alcino Cunha):
Experimental Prover back-end for Alloy or (preferably) Electrum. This could be done in several ways. One way would be to translate Alloy/Electrum models into HLL models. Another (probably simpler) way would be to translate some internal representation used by Alloy/Electrum directly to LLL.
Experimental Prover back-end for TLA+. Again this could be done in different ways, such as translating TLA+ to HLL.
Experimental translation of Solidity (Ethereum's language for writing smart contracts) to HLL.
Take any modeling/verification problem that you could have reasonably approached using Alloy or TLA+, model it in HLL and verify it using PSL. This case study would be particularly interesting, since it has already been approached using Electrum (see Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum).
Glossary:
HLL: Prover's high-level language for modeling reactive systems (predicate logic and rich data types).
LLL: Prover's low-level language for modeling reactive systems (propositional logic).
PSL: Prover's model checker.
Project proposed by J.C. Ramalho (contact person: J.N. Oliveira):
Formal modelling of a support system for a TS-RADA ontology for the M-51-CLAV platform.
Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager OPAM (disponível em Homebrew para Max OSX).
Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011)
Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Yves Bertot & Pierre Casteran. Springer (2004)
Funcionamento
Avaliação
2 testes, com nota mínima (agregada) de 8 valores (70%)
1 trabalho desenvolvido em grupo, envolvendo o estudo de um tópico (diferente para cada grupo), e possivelmente algum desenvolvimento. O trabalho deverá dar origem a um artigo a entregar no final do semestre, bem como a uma apresentação feita por todo o grupo (30%)
Dadas as circunstâncias muito particulares de funcionamento desta UC este ano lectivo, o método de avaliação foi alterado.
A avaliação será feita com base nos seguintes elementos:
2 ou 3 exercícios a serem resolvidos em casa semanalmente (e entregues por e-mail) para cada uma das duas partes do curso. Esta componente de avaliação dará origem a uma nota final de, no máximo, 15 valores.
um trabalho final opcional, envolvendo uma ou mais ferramentas estudadas no curso, para estudantes que desejam ter uma nota final superior a 15.
TWiki's Education/MFES1920 webThe Education/MFES1920 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920Copyright 2020 by contributing authors2020-09-30T19:14:09ZCSIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/CSI2020-09-30T19:14:09ZUC2 Cálculo de Sistemas de Informação Information Systems by Calculation (E Learning) Programa da UC / Course syllabus Métodos formais ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebHome2020-09-22T15:00:59ZBem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Avisos2020-09-17T14:29:30Z17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ... (last changed by JoseNunoOliveira)JoseNunoOliveiraATShttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/ATS2020-09-17T10:21:49ZAnálise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ... (last changed by JoaoSaraiva)JoaoSaraivaVFhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/VF2020-05-26T09:59:59ZUC3 Verificação Formal Programa Resumido Lógica e Sistemas de Prova Sistemas de prova automática: lógica proposicional; SAT solvers; ... (last changed by MariaJoaoFrade)MariaJoaoFradeEMhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EM2020-02-12T07:58:31ZEspecificação e Modelação Programa Lógicas para especificação e modelação Lógica de primeira ordem Lógica relacional Lógica temporal ... (last changed by AlcinoCunha)AlcinoCunhaAChttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/AC2020-02-04T15:20:00ZUC4 Arquitectura e Cálculo A página desta cadeira encontra se em http://arca.di.uminho.pt/ac 1920/. (last changed by JoseNunoOliveira)JoseNunoOliveiraLEIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/LEI2020-01-14T19:53:08ZCohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebSideBar2020-01-13T16:27:53ZTópicos Bem vindo a MFES principal Docentes Contacto Sumários OC Análise e Teste de Software UC1 Especificação e Modelação ... (last changed by JoseNunoOliveira)JoseNunoOliveiraEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EquipaDocente2019-09-17T11:04:35ZEquipa docente Soares Barbosa Alcino Cunha João Frade Moreira Macedo Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Calendario2019-09-17T10:53:38ZCalendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 17 Sep 2019 (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebPreferences2019-09-17T09:16:29ZEducation/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)AlcinoCunhaWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1920 Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic ... (last changed by TWikiGuest)TWikiGuestWebTopicActionshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunhaWebCsshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebCss2007-05-03T08:33:47Z.natRevision { width:0px; height:0px; overflow:hidden; } .natBreadCrumbs { width:0px; height:0px; overflow:hidden; } .avisos { color: #444; font size ... (last changed by AlcinoCunha)AlcinoCunhaWebTopBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopBar2007-02-13T14:43:04Z (last changed by AlcinoCunha)AlcinoCunha
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ...
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ...
Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software.
Este perfil de especialização do MiEI conta com uma equipa de docentes altamente qualificados na investigação e ensino de métodos formais aplicados ao desenvolvimento de software.
Todos fazemos parte do Laboratório HASLab/U.Minho
(Formal Methods for High-Assurance Software),
em que se vem consolidando know-how em métodos formais desde há mais de 30 anos.
As unidades curriculares que compoem MFES corporizam os principais vectores de que depende o projecto de aplicações fiáveis, à escala industrial.
Na sua componente teórica, a visão é a de abordar problemas de software segundo uma autêntica perspectiva de engenharia, que permite - através da modelos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos. Uma vez escritos, MFES ensina como fazer a sua análise e teste, dois ingredientes essenciais à qualidade do software.
O HASLab/U.Minho orgulha-se de ter sido convidado a organizar o 3º congresso mundial de MF, que terá lugar no Porto em Outubro de 2019.
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ...
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this Education/MFES1920 web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
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
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
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
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Natural Skin configuration
Set SKIN=nat
Set SKINSTYLE = Plain
Set STYLEBORDER = thin
Set STYLEBUTTONS = off
Set STYLESIDEBAR = left
Set STYLEVARIATION = none
Set STYLESEARCHBOX = off
Set PAGETITLE = Métodos Formais em Engenharia de Software
Set NATWEBLOGO = Métodos Formais em Engenharia de Software
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
Set WEBLOGOALT = Métodos Formais em Engenharia de Software
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/MFES1920.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Métodos Formais em Engenharia de Software
Set SITEMAPUSETO = Mestrado Integrado em Engenharia Informática - MFES 2019/2020
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
Set NOSEARCHALL =
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Education/MFES1920 web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920
The Education/MFES1920 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Education/MFES1920
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920
/twiki/pub/Main/LocalLogos/um_eengP.jpgCSI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/CSI
UC2 Cálculo de Sistemas de Informação Information Systems by Calculation (E Learning) Programa da UC / Course syllabus Métodos formais ... (last changed by JoseNunoOliveira)2020-09-30T19:14:09ZJoseNunoOliveiraWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebHome
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)2020-09-22T15:00:59ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Avisos
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ... (last changed by JoseNunoOliveira)2020-09-17T14:29:30ZJoseNunoOliveiraATS
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/ATS
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ... (last changed by JoaoSaraiva)2020-09-17T10:21:49ZJoaoSaraivaVF
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/VF
UC3 Verificação Formal Programa Resumido Lógica e Sistemas de Prova Sistemas de prova automática: lógica proposicional; SAT solvers; ... (last changed by MariaJoaoFrade)2020-05-26T09:59:59ZMariaJoaoFradeEM
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EM
Especificação e Modelação Programa Lógicas para especificação e modelação Lógica de primeira ordem Lógica relacional Lógica temporal ... (last changed by AlcinoCunha)2020-02-12T07:58:31ZAlcinoCunhaAC
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/AC
UC4 Arquitectura e Cálculo A página desta cadeira encontra se em http://arca.di.uminho.pt/ac 1920/. (last changed by JoseNunoOliveira)2020-02-04T15:20:00ZJoseNunoOliveiraLEI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/LEI
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ... (last changed by JoseNunoOliveira)2020-01-14T19:53:08ZJoseNunoOliveiraWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebSideBar
Tópicos Bem vindo a MFES principal Docentes Contacto Sumários OC Análise e Teste de Software UC1 Especificação e Modelação ... (last changed by JoseNunoOliveira)2020-01-13T16:27:53ZJoseNunoOliveiraEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EquipaDocente
Equipa docente Soares Barbosa Alcino Cunha João Frade Moreira Macedo Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)2019-09-17T11:04:35ZJoseNunoOliveiraCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Calendario
Calendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 17 Sep 2019 (last changed by JoseNunoOliveira)2019-09-17T10:53:38ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebPreferences
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)2019-09-17T09:16:29ZAlcinoCunhaWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebCss
.natRevision { width:0px; height:0px; overflow:hidden; } .natBreadCrumbs { width:0px; height:0px; overflow:hidden; } .avisos { color: #444; font size ... (last changed by AlcinoCunha)2007-05-03T08:33:47ZAlcinoCunhaWebTopBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopBar
(last changed by AlcinoCunha)2007-02-13T14:43:04ZAlcinoCunhaWebLeftBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebLeftBar
Apresentação Sumários Projectos Material (last changed by AlcinoCunha)2007-02-13T10:35:33ZAlcinoCunha
AVISO (31/1): Final do torneio do CodeDefender?Live: foto.
AVISO (27/1): A final do torneio do CodeDefender? é 6a feira, dia 31/1 às 15:00 (no Aquário do piso 2 do DI).
AVISO (23/1): O exame é dia 28/1 às 9am (sala CP1-1.10).
- Nesse dia de tarde (14:00-16:00, sala de reuniões do DI) daremos um tutorial sobre Selenium (teste de applicações web), no contexto do programa doutoral MAPi: os alunos de ATS estão convidados a assistir.
- Ás 16:00 tentaremos fazer a final do torneio CodeDefender? (a confirmar com os finalistas).
- Até ao fim do dia 27/1 os alunos deverão enviar num ficheiro zip com o trabalho (todo o código) + relatório + slides para ats.2019.2020@gmail.com
AVISO (21/1): A apresentação do trabalho e torneio é na sala DI-1.09.
AVISO (17/1): O horário da apresentação dos projetos e do torneio pode ser consultado no link:
Apresentação + Torneio
- Quem não tiver grupo (ver secção Grupos) deve enviar email para os docentes (há dois grupos de reserva).
- Os grupo podem trocar de horário de apresentação/torneio desde que ambos grupos concordem.
- Na apresentação todos os membros do grupo devem estar presentes.
- Os grupos devem entregar o relatório impresso.
AVISO (15/1): As notas do teste estão disponíveis na secção da availação.
O teste pode ser consultado, 2a feira, dia 20/1, às 10am (no gabinete DI:2.09)
O torneio CodeDefender? será realizado em simultâneo com as apresentações do projeto.
AVISO (13/1): A entrega e apresentação do projeto será realizada no 3a feira, dia 21 de Janeiro.
A apresentação consiste em duas partes: Na 1a parte os grupos devem preparar uma pequena apresentação (10 minutos) onde devem descrever o que fizeram e os resultados atingidos. A 2a parte consiste numa "tool demo" da aplicação desenvolvida, que deverá também ser preparada com cuidado. No total a apresentação é de 30 mintos.
Em breve será definida o horário de apresentação de cada um dos grupos.
As notas do teste serão aqui disponibilizadas esta 4a feira.
Equipa Docente
João Saraiva: aula teóricas
José Nuno Macedo: aulas laboratoriais
Aula 0 (17/09): Apresentação da disciplina.
Aula 1 (01/10): (T + PL) Combinadores de Parsing. "Embedded Domain Specific Languages". Gramáticas (BNF) como uma EDSL em Haskell: Combinadores de Parsing.
Aula 2 (08/10): (T + PL) Semântica Estática de Linguagens de Programação: Análise de Nomes.
Aula 3 (15/10): (T + PL) Software Metrics e Code Smells. O sistema SonarQube.
Aula 4 (22/10):
T: Software Refactoring: Introdução e Apresentação do catálogo de Java. Software "Technical Debt".
TP: Aplicação de Refactorings disponíveis no IntelliJ? a software Java.
Aula 5 (29/10):
T: Análise de Consumo de Energia: Introdução a Green Software.
TP: Apresentação da framework RAPL para monitorizar o consumo de energia. Resolução de Exercícios.
Aula 6 (05/11):
T: Teste de Sofware: Introdução. Cobertura de Testes.
TP: Apresentação da framework de teste unitário JUnit (e HUnit). Resolução de Exercícios.
Aula 7 (12/11):
T: Geração Automática de Casos de Teste.
TP: Apresentação do sistema QuickCheck? . Resolução de Exercícios.
Aula 8 (19/11):
T: Geração Automática de Casos de Teste: Continuação.
TP: Apresentação do sistema EvoSuite? . Resolução de Exercícios.
Aula 9 (26/11): T: Teste de Propriedades.
TP: Resolução de Exercícios em QuickCheck?Aula 10 (03/12): T: Análise da Qualidade dos Testes via Mutações.
TP: O sistema de mutação de testes PIT. Resolução de exercícios.
Aula 11 (10/12): T: Localização de Falhas. Correção Automática de Programas TP: Teste de aplicações Web: A framework Selenium. "Gamefication" da tarefa de Teste de Software: Competição entre os grupos de projeto.
Aula 12 (17/12): T + TP: Teste Individual.
Fichas de Exercícios
Ficha 1: Combinadores de Parsing
*Parsing.pdf*
Ficha 2: Static Semantics
*Semantics.pdf*
Ficha 3: Refactoring
Refactoring.pdf
Ficha 4: Unit Testing & Cobertura
*Testing.Cobertura.pdf*
Ficha 5: Geração de Casos de Teste em QuickCheck?Geração de Valores.pdf
Ficha 6: Geração de Testes Unitários em EvoSuite?EvoSuite.pdf
Ficha 7: Teste de Propriedades em QuickCheck?property_testing.pdfFicha 8: Mutação de Testes Mutation-Testing.pdfEntrega da Geração Automática de Logs: A solução da geração automática de inputs para a aplicação UmCarroJa? ! deve ser entregue enviando a solução para o seguinte email: ats.2019.2020@gmail.com
O email deve ter o título: Entrega - Logs da UmCarroJa? ! e incluir o nome dos elementos do grupo. Em anexo deve ser incluído um ficheiro zip com todo o código da solução. Deve ainda ser incluído um ficheiro readme.txt onde se descreve como executar o software.
Data Limite: 04 de Dezembro (PT time)
Software
1- Combinadores de Parsing: Biblioteca desenvolvida na aula: *Parser.hs*Exemplo desenvolvido na aula:Lang.hs2-Projeto UMCarroJa?(desenvolvido pelos alunos na dsciplina de POO): enunciado.pdfSoluções dos alunos: p1.zip e
p2.zip3-Projetos Java: Poligono (Poligono.zip) e Contactos (Contactos.zip)
4-Monitorização do Consumo de Energia:Rapl.tar.gz
Projeto em Grupo
O enúnciado do projeto a desenvolver em grupo está disponível aqui(versão atualizada em 19/11)Ficheiro de Log para execução em batch:logsPOO_carregamentoInicial.bak
Regime de Avaliação
A avaliação consiste em três componentes: prova individual (PI) (teste ou exame escritos), Projeto em Grupo (PG) (a resolver durante o semestre) e Avaliação Contínua (AC) (com base em problemas propostos nas aulas TP). As provas escritas são de consulta de material impresso, apenas.
A Nota final é calcula de acordo com a seguinte fórmula: 40% PI + 40% PG + 20% AC, com nota mínima de 8 valores em todas as componentes de avaliação.
O teste individual é de consulta: os alunos podem consultar todo o material (não eletrónico) que tiverem consigo.
Datas da Avaliação
Prova Individual:: 17/12/2019(última aula de 2019)Exame:: 28/01/2020(a confirmar)Entrega do Projeto em Grupo:14/01/2020(a confirmar)
17 Set - Vídeo de apresentação da edição de 2020/21.
30 Mar - VF: alteração do método de avaliação. 21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.
10 Fev - CSI: afixadas as notas finais na página de CSI.
4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.
28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.
26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.
13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.
13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.
13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.
13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.
5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.
2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.
3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.
24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.
12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.
10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.
29 Out - CSI: Formulário actualizado colocado na página respectiva.
2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.
26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).
17 Set - Início das aulas: 17-Set (ATS).
-- JoseNunoOliveira - 17 Sep 2019
Métodos formais e qualidade de software. Conceitos básicos: modelo, especificação, verificação e prova.
As relações binárias polimórficas como linguagem de especificação formal universal. Setas e diagramas. Estudo do cálculo relacional 'pointfree'. Conexões de Galois. Polimorfismo paramétrico.
O papel das funções na taxonomia das relações binárias. Teorema grátis de uma função polimórfica.
Atributos e dependências funcionais. O modelo de dados 'pares valores-chave' construído com relações simples, emparelhamentos e coprodutos. Integridade referencial.
Preservação de invariantes e satisfação. Cálculo da precondição mais fraca 'wp (f, p)' para uma dada função 'f' e invariante 'p'. Relações (invariantes) como tipos.
'Design by contract' por cálculo apoiado por model-checking.
Breve estudo da interpretação abstracta. Funções invariantes. Simulação relacional. Propriedades de segurança e de animação. Redução do espaço de estados por interpretação abstrata.
Formal methods for software quality. Basic concepts: model, specification, verification and proof.
Polymorphically typed binary relations as a universal formal specification language. Arrows and diagrams. Binary relations in Alloy. Study of the pointfree relational calculus. Galois connections. Parametricity.
The role of functions in the taxonomy of binary relations. Relations as types, inc. data type invariants. Theorems for free.
Attributes and functional dependencies. Key-value-pair data model = relational simplicity + pairing + coproducts. Referential integrity.
Data type invariants: preservation and satisfiability. Calculation of weakest preconditions for invariant preservation.
'Design by contract': combining model-checking with algebraic calculation. Refinement ordering on relations.
Brief study of abstract interpretation. Invariant functions. Relational simulation. Safety and liveness properties relationally. Reducing the state space by abstract interpretation.
Duas provas de avaliação (mini-teste + teste) e exame de recurso.
Avaliação contínua com base em problemas dados nas aulas TP.
As provas escritas são de consulta de material impresso, apenas.
O mini-teste é eliminatório de matéria para o teste e vale 50%.
Bibliografia
J.N. Oliveira. Program Design by Calculation (, 1.9Mb), Departamento de Informática, Universidade do Minho. Os capítulos deste livro (em preparação, a versão actual é de Fev. 2019) essenciais para esta disciplina no corrente ano lectivo são o quinto, o sexto e o sétimo.
Formulário CSI: ( 137K) - Leis do cálculo relacional básico.
Caso de estudo: ( 127K) - Especificação relacional do calendário de um campeonato de futebol (e sua conversão para Alloy).
Caso de estudo: ( 52K) - Especificação relacional do problema da 'merceraria da D. Acácia' (com modelo Alloy).
Script alloy.sed para converter instâncias geradas pelo Alloy para Haskell - em Alloy, visualizar instância em modo Txt e copiar para ficheiro, eg. i.txt; de seguida fazer, numa shell, sed -f alloy.sed i.txt
Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.
Módulo Alloy: prod.als - produtos cartesianos em Alloy.
Biblioteca Haskell: RelCalc.hs - Cálculo relacional básico em Haskell (precisa da biblioteca Cp).
Q01 - Como é que se deve abordar o exercício 5.22? Parece muito trabalhoso...R: O que se pede é provar que a composição preserva os 4 critérios principais (injectividade, sobrejectividade, etc). Mas basta provar que preserva a injectividade e sobrejectividade apenas, pois os outros casos derivam desses por (5.34) e (5.35). Vejamos como provar que a composição preserva a injectividade (NB: completar / estudar as justificações). São dadas R e S injectivas:
(R . S ) é injectiva
<=> { definição }
ker (R . S ) ⊆ id
<=> { def kernel }
ker ( S◦ . R◦ . R . S ) ⊆ id
<= { R injectiva (R◦ . R ⊆ id) por hipótese; regra do ponto-médio B }
ker ( S◦ . S ) ⊆ id
<= { S injectiva (S◦ . S ⊆ id) por hipótese; regra do ponto-médio B }
id ⊆ id
<= { trivial }
true
Q02 - Consigo ver que o exercício 5.21 deverá basear-se nas leis (5.62) e (5.63) mas não consigo completar o raciocínio. Como devo prosseguir?R: Ou S vai ser simples e R injectiva ou vice-versa. Coloquemos a primeira hipótese:
(P ∩ Q)·S = (P·S) ∩ (Q·S)
<= { (5.62) }
P · img S ⊆ P ∨ Q · img S ⊆ Q
<= { img S ⊆ id por hipótese; regra do ponto-médio B }
P · id ⊆ P ∨ S · id ⊆ S
<= { P · id = P etc }
true
Agora é só verificar R·(P∩Q) = (R·P)∩(R·Q) para R injectiva, seguindo o mesmo método.
Q03 - Na resolução da questão 4 do teste do ano passado há uma altura em que chego a qualquer coisa como dE . V . i1◦ ⊆ Di . i1◦. Por monotonia da composição (. i1◦) consigo ver que dE . V ⊆ Di implica dE . V . i1◦ ⊆ Di . i1◦. Mas eu preciso que sejam equivalentes. Sugestões?R: Por 'shunting' de i1◦ do termo inferior para o superior (sem o converso), obtém-se i1◦ . i1 nesse lado. Ora i1◦ . i1 = id pois i1 (e i2) são injecções (funções injectivas, cujo núcleo é id). Basta então 'cortar' i1◦ . i1, não havendo perda da equivalência.
Q04 - Não sei como pegar no exercício 5.24...R: Este tipo de exercícios deve ser abordado usando monotonia ou regras de algibeira como (5.82, 5.83) etc. Exemplo: sabemos que R ∩ S ⊆ R fazendo X := R ∩ S na propriedade (5.58) e simplificando. Vamos supor que R é simples. Como "menor que simples é sempre simples" (5.82) então R ∩ S será simples. Etc para os outros casos.
Q05 - Como é que se aplica a igualdade indirecta no exercício 5.46? Não consigo ver como.R: A igualdade c◦ · (⊤ − c) = ⊥ é equivalente a c◦ ·(⊤−c) ⊆ ⊥. Por (5.151) podemos subir o lado inferior, para c◦ ·(c⇒⊥) ⊆ ⊥. A partir daí aplica-se a (5.154), obtendo-se (c◦ ·c⇒⊥) ⊆ ⊥. Agora é que se pode aplicar a igualdade indirecta para mostrar que c◦ ·c⇒⊥ = ⊥.
Q06 - Não estou a conseguir fazer a primeira prova do exercício 5.37. Como é que se pega na questão?R: Ora vejamos:
[R,S]·[T,U]◦
= { (5.117) }
(R·i1◦ ∪ S·i2◦) · [T,U]◦
= { justificar }
(R·i1◦·[T,U]◦) ∪ (S·i2◦·[T,U]◦)
= { justificar }
R·([T,U]·i1)◦ ∪ S·([T,U]·i2)◦
.... (Agora é só continuar)
Q07 - Ao resolver uns exercícios deparei-me com uma dúvida: R◦ × S◦ = (R × S)◦ verifica-se?R: Sim, verifica-se, como facilmente se prova: ( R × S )◦ = ⟨R·π1,S·π2⟩◦ = (π1◦ · R·π1 ∩ π2◦ · S·π2)◦ = R◦ × S◦
Q08 - Consegui resolver a primeira prova do 5.39 mas não estou a conseguir resolver a segunda...R: Na segunda usam-se as propriedades dos coprodutos. Por exemplo, se se começar por (g+k)◦ . (f + h), como (f + h) = [ i1.f, i2.h],
usa-se fusão-+ (relacional, igual à funcional) e fica-se com [(g◦+k◦).i1.f,(g◦+k◦).i2.h] (onde também se usou 5.123). De seguida obtém-se [i1.g◦.f,i2.k◦.h], que é igual a f/g + h/k.
Q09 - No teste, para quem realizar a 2ª parte da matéria, excluindo a matéria do mini-teste, que capítulos sairão?R: A matéria que foi dada depois do miniteste é a seguinte: secções 5.20, 5.21, 5.24 e capítulo 7.
Q10 - Não consigo perceber a justificação ao fundo da página 255.R: É de esperar, já que a justificação está muito imprecisa. Em geral, as funções constantes são tudo menos injectivas (!). Mas, aqui, o tipo de const c é 1 -> N0 (vejam porquê). Logo, const c é injectiva, pois o seu núcleo é de tipo 1 -> 1 e a maior relação possível nesse tipo é id : 1->1. (Agradeço esta dúvida, pois permitiu melhorar já a justificação que irá sair na próxima versão dos apontamentos.)
Q11 - Na última questão do teste de 17/18 não consigo justificar o terceiro e o quarto passo.R: As justificações são as seguintes: 3) teorema grátis de swap; 4) (F8), após fazer-se 'shunting' de θº.
Q12 - Na questão 6 do teste do ano passado não consigo justificar o segundo passo.R: Fazendo 'shunting' de splitAt da esquerda para a direita em splitAt ⊆ ((R* × R*) ← R*) · splitAt ficamos com id ⊆ splitAtº .((R* × R*) ← R*) · splitAt. De seguida introduzimos variáveis, eg. n e n'. Como n id n' é n=n', uma dessas variáveis desaparece.
Q13 - Não sei como justificar o penúltimo passo da questão 7 (segunda parte) do teste de 17/18.R: Dos quatro termos que estão a ser reunidos, se se isolar i1·(R◦·R)·i1◦ ∪ i2·(S·S)·i2◦, verifica-se que essa reunião é ker R + ker S por aplicação das leis dos coprodutos (R+S = [ i1· R, i2· S ] etc).
Q14 - Não percebo qual a razão para a cláusula 'injective(const e· (const c)◦)' desaparecer no penúltimo passo da prova sugerida para a questão 7 do teste de 18/19.R: Uma relação R é injectiva sse ker R ⊆ id. Neste caso, R = const e· (const c)◦, logo ker R = const c . (const e)◦ . const e· (const c)◦ ⊆ id. Se fizermos os 'shuntings' do costume, obtém-se ker R ⊆ id ≡ ⊤ ⊆ ⊤, por (6.28).
Links
History of Formal Methods - links referidos na primeira aula teórica:
Os carros modernos oferecem várias funcionalidades de segurança e conforto baseadas em componentes de software. Em particular, são já comuns atualmente sistemas de luzes exteriores adaptativos e de controlo de velocidade. Estes sistemas recolhem informação tanto de sensores (e.g., de luminosidade ou de velocidade) e da interface com o condutor (e.g., botões ou opções no computador de bordo), que é depois usada para controlar os atuadores (e.g., luzes externas ou os travões). É também comum que estes sistemas sejam adaptáveis para diferentes mercados (e.g., carros vendidos na UE ou nos EUA têm que seguir diferentes regras). O seguinte apontador descreve possíveis requisitos para sistemas deste tipo, e foi lançado como desafio numa conferência sobre métodos formais como os que estudamos nesta UC. Disponibiliza também um conjunto de sequências de validação que exemplificam possíveis execuções do sistema.
Os grupos de trabalho devem estudar o documento de referência referido acima com atenção, por forma a perceberem bem qual é o problema que é abordado. Naturalmente, devido à natureza das ferramentas, aspetos contínuos como o tempo real e a velocidade terão que ser abstraídos. Não é também expectável que cada grupo modele todas as componentes do sistema, ficando à consideração de cada um que aspetos focar. O modelo deve no entanto ser suficientemente rico em estrutura e comportamento, e permitir a verificação de alguns dos requisitos. Algumas sugestões são:
Focar-se apenas num sistema (e.g., o de luzes exteriores)
Focar-se apenas numa das funcionalidade do sistema (e.g., luzes de direção)
Focar-se apenas numa configuração concreta (e.g., mercado EU)
Trabalho 1 sobre Alloy/Electrum
O objetivo deste trabalho é desenvolver um modelo Electrum de (uma parte) deste sistema, assim como um theme que facilite a compreensão das instâncias. Os grupos deverão entregar por email o trabalho até à data limite de 4-Dec-2019 (um modelo Electrum, devidamente comentado, e o respetivo theme).
Trabalho 2 sobre SMV/TLA+
O objetivo deste trabalho é desenvolver um modelo em SMV ou TLA+ de (uma parte) deste sistema. Os grupos deverão entregar por email o trabalho até à data limite de 15-Jan-2020 (um modelo SMV ou TLA+, devidamente comentado).
Project ideas from Prover Technology (if you are interested in any of these projects please contact Alcino Cunha):
Experimental Prover back-end for Alloy or (preferably) Electrum. This could be done in several ways. One way would be to translate Alloy/Electrum models into HLL models. Another (probably simpler) way would be to translate some internal representation used by Alloy/Electrum directly to LLL.
Experimental Prover back-end for TLA+. Again this could be done in different ways, such as translating TLA+ to HLL.
Experimental translation of Solidity (Ethereum's language for writing smart contracts) to HLL.
Take any modeling/verification problem that you could have reasonably approached using Alloy or TLA+, model it in HLL and verify it using PSL. This case study would be particularly interesting, since it has already been approached using Electrum (see Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum).
Glossary:
HLL: Prover's high-level language for modeling reactive systems (predicate logic and rich data types).
LLL: Prover's low-level language for modeling reactive systems (propositional logic).
PSL: Prover's model checker.
Project proposed by J.C. Ramalho (contact person: J.N. Oliveira):
Formal modelling of a support system for a TS-RADA ontology for the M-51-CLAV platform.
Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager OPAM (disponível em Homebrew para Max OSX).
Logic in Computer Science: Modelling and Reasoning About Systems. Michael Huth & Mark Ryan. Cambridge University Press; 2nd edition (2004).
The Calculus of Computation: Decision Procedures with Applications to Verification. Aaron R. Bradley & Zohar Manna. Springer (2007).
Rigorous Software Development: An Introduction to Program Verification. J.B. Almeida & M.J. Frade & J.S. Pinto & S.M. de Sousa. Springer (2011)
Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Yves Bertot & Pierre Casteran. Springer (2004)
Funcionamento
Avaliação
2 testes, com nota mínima (agregada) de 8 valores (70%)
1 trabalho desenvolvido em grupo, envolvendo o estudo de um tópico (diferente para cada grupo), e possivelmente algum desenvolvimento. O trabalho deverá dar origem a um artigo a entregar no final do semestre, bem como a uma apresentação feita por todo o grupo (30%)
Dadas as circunstâncias muito particulares de funcionamento desta UC este ano lectivo, o método de avaliação foi alterado.
A avaliação será feita com base nos seguintes elementos:
2 ou 3 exercícios a serem resolvidos em casa semanalmente (e entregues por e-mail) para cada uma das duas partes do curso. Esta componente de avaliação dará origem a uma nota final de, no máximo, 15 valores.
um trabalho final opcional, envolvendo uma ou mais ferramentas estudadas no curso, para estudantes que desejam ter uma nota final superior a 15.
TWiki's Education/MFES1920 webThe Education/MFES1920 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920Copyright 2020 by contributing authors2020-09-30T19:14:09ZCSIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/CSI2020-09-30T19:14:09ZUC2 Cálculo de Sistemas de Informação Information Systems by Calculation (E Learning) Programa da UC / Course syllabus Métodos formais ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebHome2020-09-22T15:00:59ZBem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Avisos2020-09-17T14:29:30Z17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ... (last changed by JoseNunoOliveira)JoseNunoOliveiraATShttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/ATS2020-09-17T10:21:49ZAnálise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ... (last changed by JoaoSaraiva)JoaoSaraivaVFhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/VF2020-05-26T09:59:59ZUC3 Verificação Formal Programa Resumido Lógica e Sistemas de Prova Sistemas de prova automática: lógica proposicional; SAT solvers; ... (last changed by MariaJoaoFrade)MariaJoaoFradeEMhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EM2020-02-12T07:58:31ZEspecificação e Modelação Programa Lógicas para especificação e modelação Lógica de primeira ordem Lógica relacional Lógica temporal ... (last changed by AlcinoCunha)AlcinoCunhaAChttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/AC2020-02-04T15:20:00ZUC4 Arquitectura e Cálculo A página desta cadeira encontra se em http://arca.di.uminho.pt/ac 1920/. (last changed by JoseNunoOliveira)JoseNunoOliveiraLEIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/LEI2020-01-14T19:53:08ZCohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebSideBar2020-01-13T16:27:53ZTópicos Bem vindo a MFES principal Docentes Contacto Sumários OC Análise e Teste de Software UC1 Especificação e Modelação ... (last changed by JoseNunoOliveira)JoseNunoOliveiraEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EquipaDocente2019-09-17T11:04:35ZEquipa docente Soares Barbosa Alcino Cunha João Frade Moreira Macedo Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Calendario2019-09-17T10:53:38ZCalendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 17 Sep 2019 (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebPreferences2019-09-17T09:16:29ZEducation/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)AlcinoCunhaWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1920 Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic ... (last changed by TWikiGuest)TWikiGuestWebTopicActionshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunhaWebCsshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebCss2007-05-03T08:33:47Z.natRevision { width:0px; height:0px; overflow:hidden; } .natBreadCrumbs { width:0px; height:0px; overflow:hidden; } .avisos { color: #444; font size ... (last changed by AlcinoCunha)AlcinoCunhaWebTopBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopBar2007-02-13T14:43:04Z (last changed by AlcinoCunha)AlcinoCunha
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ...
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ...
Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software.
Este perfil de especialização do MiEI conta com uma equipa de docentes altamente qualificados na investigação e ensino de métodos formais aplicados ao desenvolvimento de software.
Todos fazemos parte do Laboratório HASLab/U.Minho
(Formal Methods for High-Assurance Software),
em que se vem consolidando know-how em métodos formais desde há mais de 30 anos.
As unidades curriculares que compoem MFES corporizam os principais vectores de que depende o projecto de aplicações fiáveis, à escala industrial.
Na sua componente teórica, a visão é a de abordar problemas de software segundo uma autêntica perspectiva de engenharia, que permite - através da modelos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos. Uma vez escritos, MFES ensina como fazer a sua análise e teste, dois ingredientes essenciais à qualidade do software.
O HASLab/U.Minho orgulha-se de ter sido convidado a organizar o 3º congresso mundial de MF, que terá lugar no Porto em Outubro de 2019.
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ...
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ...
This is a subscription service to be automatically notified by e-mail when topics change in this Education/MFES1920 web. This is a convenient service, so you do not have to come back and check all the time if something has changed. To subscribe, please add a bullet with your WikiName in alphabetical order to this list:
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
Subscribe Daisy to all changes in all webs that start with Web.
* daisy.cutter@flowers.com: Web*
Subscribe Daisy to changes to topics starting with Petal, and their immediate children, WeedKillers and children to a depth of 3, and all topics that match start with Pretty and end with Flowers e.g. PrettyPinkFlowers
Subscribe Daisy to the full content of NewsLetter whenever it has changed
* daisy@flowers.com: TWiki.NewsLetter?
Subscribe buttercup to NewsLetter and its immediate children, even if it hasn't changed.
* buttercup@flowers.com: TWiki.NewsLetter! (1)
Subscribe GardenGroup (which includes Petunia) to all changed topics under AllnewsLetters to a depth of 3. Then unsubscribe Petunia from the ManureNewsLetter, which she would normally get as a member of GardenGroup? :
A user may be listed many times in the WebNotify topic. Where a user has several lines in WebNotify that all match the same topic, they will only be notified about changes that topic once (though they will still receive individual mails for news topics).
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
These settings override the defaults for this web only. See full list of defaults with explanation. Many of the settings below are commented out. Remove the # sign to enable a local customisation.
Natural Skin configuration
Set SKIN=nat
Set SKINSTYLE = Plain
Set STYLEBORDER = thin
Set STYLEBUTTONS = off
Set STYLESIDEBAR = left
Set STYLEVARIATION = none
Set STYLESEARCHBOX = off
Set PAGETITLE = Métodos Formais em Engenharia de Software
Set NATWEBLOGO = Métodos Formais em Engenharia de Software
Web-specific background color: (Pick a lighter one of the StandardColors).
Set WEBBGCOLOR = #D0D0D0
Note: This setting is automatically configured when you create a web
Image, URL and alternate tooltip text of web's logo. Note: Don't add your own local logos to the TWikiLogos topic; create your own logos topic instead.
Set WEBLOGOALT = Métodos Formais em Engenharia de Software
List this web in the SiteMap. If you want the web listed, then set SITEMAPLIST to on, do not set NOSEARCHALL, and add the "what" and "use to..." description for the site map. Use links that include the name of the web, i.e. Education/MFES1920.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Métodos Formais em Engenharia de Software
Set SITEMAPUSETO = Mestrado Integrado em Engenharia Informática - MFES 2019/2020
Note: Above settings are automatically configured when you create a web
Exclude web from a web="all" search: (Set to on for hidden webs).
Set NOSEARCHALL =
Note: This setting is automatically configured when you create a web
Prevent automatic linking of WikiWords and acronyms (if set to on); link WikiWords (if empty); can be overwritten by web preferences:
#Set NOAUTOLINK =
Note: You can still use the [[...][...]] syntax to link topics if you disabled WikiWord linking. The <noautolink> ... </noautolink> syntax can be used to prevents links within a block of text.
Default template for new topics for this web:
WebTopicEditTemplate? : Default template for new topics in this web. (Site-level is used if topic does not exist)
Comma separated list of forms that can be attached to topics in this web. See TWikiForms for more information.
Set WEBFORMS =
Users or groups who are not / are allowed to view / change / rename topics in the Education/MFES1920 web: (See TWikiAccessControl). Remove the # to enable any of these settings. Remember that an empty setting is a valid setting; setting DENYWEBVIEW to nothing means that anyone can view the web.
Preferences are used as TWikiVariables by enclosing the name in percent signs. Example:
When you write variable %WEBBGCOLOR% , it gets expanded to #D0D0D0
The sequential order of the preference settings is significant. Define preferences that use other preferences first, i.e. set WEBCOPYRIGHT before WIKIWEBMASTER since %WEBCOPYRIGHT% uses the %WIKIWEBMASTER% variable.
You can introduce your own preferences variables and use them in your topics and templates.
TWiki search results for \.*
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920
The Education/MFES1920 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.en-usCopyright 2020 by contributing authorsTWiki Administrator [webmaster@di.uminho.pt]The contributing authors of TWikiTWikiDIUM.Education/MFES1920
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920
/twiki/pub/Main/LocalLogos/um_eengP.jpgCSI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/CSI
UC2 Cálculo de Sistemas de Informação Information Systems by Calculation (E Learning) Programa da UC / Course syllabus Métodos formais ... (last changed by JoseNunoOliveira)2020-09-30T19:14:09ZJoseNunoOliveiraWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebHome
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2019/20 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)2020-09-22T15:00:59ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Avisos
17 Set Vídeo de apresentação da edição de 2020/21. 30 Mar VF: alteração do método de avaliação. 21 Fev VF: aula de substituição será, 4ª feira, 26 Fev ... (last changed by JoseNunoOliveira)2020-09-17T14:29:30ZJoseNunoOliveiraATS
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/ATS
Análise e Teste de Software AVISO (31/1): Final do torneio do CodeDefender Live : foto. AVISO (27/1): A final do torneio do CodeDefender é 6a feira, dia 31/1 ... (last changed by JoaoSaraiva)2020-09-17T10:21:49ZJoaoSaraivaVF
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/VF
UC3 Verificação Formal Programa Resumido Lógica e Sistemas de Prova Sistemas de prova automática: lógica proposicional; SAT solvers; ... (last changed by MariaJoaoFrade)2020-05-26T09:59:59ZMariaJoaoFradeEM
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EM
Especificação e Modelação Programa Lógicas para especificação e modelação Lógica de primeira ordem Lógica relacional Lógica temporal ... (last changed by AlcinoCunha)2020-02-12T07:58:31ZAlcinoCunhaAC
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/AC
UC4 Arquitectura e Cálculo A página desta cadeira encontra se em http://arca.di.uminho.pt/ac 1920/. (last changed by JoseNunoOliveira)2020-02-04T15:20:00ZJoseNunoOliveiraLEI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/LEI
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ... (last changed by JoseNunoOliveira)2020-01-14T19:53:08ZJoseNunoOliveiraWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebSideBar
Tópicos Bem vindo a MFES principal Docentes Contacto Sumários OC Análise e Teste de Software UC1 Especificação e Modelação ... (last changed by JoseNunoOliveira)2020-01-13T16:27:53ZJoseNunoOliveiraEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/EquipaDocente
Equipa docente Soares Barbosa Alcino Cunha João Frade Moreira Macedo Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)2019-09-17T11:04:35ZJoseNunoOliveiraCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/Calendario
Calendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 17 Sep 2019 (last changed by JoseNunoOliveira)2019-09-17T10:53:38ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebPreferences
Education/MFES1920 Web Preferences The following settings are web preferences of the Education/MFES1920 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)2019-09-17T09:16:29ZAlcinoCunhaWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebCss
.natRevision { width:0px; height:0px; overflow:hidden; } .natBreadCrumbs { width:0px; height:0px; overflow:hidden; } .avisos { color: #444; font size ... (last changed by AlcinoCunha)2007-05-03T08:33:47ZAlcinoCunhaWebTopBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebTopBar
(last changed by AlcinoCunha)2007-02-13T14:43:04ZAlcinoCunhaWebLeftBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1920/WebLeftBar
Apresentação Sumários Projectos Material (last changed by AlcinoCunha)2007-02-13T10:35:33ZAlcinoCunha
17 Set - Vídeo de apresentação da edição de 2020/21.
30 Mar - VF: alteração do método de avaliação. 21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.
10 Fev - CSI: afixadas as notas finais na página de CSI.
4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.
28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.
26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.
13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.
13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.
13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.
13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.
5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.
2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.
3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.
24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.
12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.
10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.
29 Out - CSI: Formulário actualizado colocado na página respectiva.
2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.
26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).
17 Set - Início das aulas: 17-Set (ATS).
-- JoseNunoOliveira - 17 Sep 2019
17 Set - Vídeo de apresentação da edição de 2020/21.
30 Mar - VF: alteração do método de avaliação. 21 Fev - VF: aula de substituição será, 4ª feira, 26-Fev, às 14:00, na sala 0.04 do DI.
10 Fev - CSI: afixadas as notas finais na página de CSI.
4 Fev - As aulas de AC e VF iniciam-se esta quinta-feira, 6-Fev.
28 Jan - CSI: o exame de recurso terá lugar na sala E2-1.10 às 9h00.
26 Jan - CSI: estão lançadas as classificações após a realização do teste - ver página CSI. Atendimento para mostrar os testes: dia 27-Jan, às 16h.
13 Jan - CSI: a aula de dúvidas amanhã de tarde será às 17h, na sala 0.09, e não às 16h, como por lapso disse a alguns alunos. Pf ver Sumarios.
13 Jan - CSI: matéria para a parte 2 do teste - ver FAQ 9 na página de CSI.
13 Jan - CSI: o teste terá lugar no dia 16-Jan às 14h, na sala E7-0.07.
13 Jan - CSI: haverá uma aula de dúvidas amanhã de tarde, na sala 0.09, pf ver Sumarios.
5 Jan - EM: o prazo para a entrega do TP2 foi adiado uma semana.
2 Jan - CSI: estão lançadas as classificações do mini-teste na página CSI.
3 Dez - CSI: os alunos devem prestar atenção ao material pedagógico que vai aparecendo na página da disciplina.
24 Nov - CSI: os alunos devem prestar atenção às FAQs que vão saindo na página da disciplina.
12 Nov - CSI: mini-teste terá lugar no dia 28-Nov às 14h, na sala E7-0.07. Haverá aula depois até às 17h.
10 Nov - CSI: Caso de estudo da aula de 7-Nov ('campeonato de futebol') adicionado ao material da disciplina.
29 Out - CSI: Formulário actualizado colocado na página respectiva.
2 Out - Atenção à mudança de sala de ATS: passa para CP2.-2.08.
26 Set - Atenção à mudança de sala de CSI: passa da 1.10 para a 0.07 (Edifício 7).
17 Set - Início das aulas: 17-Set (ATS).
-- JoseNunoOliveira - 17 Sep 2019
2020/21.
30 Mar - VF: alteração do método de avaliação. 
Todos fazemos parte do Laboratório 
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 
Rename, move or delete this web: 
If you already know the name of the topic, enter the name of the topic into the 
List topics that start with the letter: 
Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.