Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos.
A página oficial da cadeira encontrar-se-á em http://arca.di.uminho.pt/ac-1819.
A avaliação dos alunos é feita tendo em conta três componentes:
Nota do Teste individual (NT)
Nota do Projecto em grupo (NP)
Avaliação Contínua (AC)
de acordo com a fórmula:
nota final = 0.45 * NT + 0.45 * NP + 0.1 * AC
Nas componentes NT e NP é obrigatório o aluno ter uma nota mínima de 8 valores.
7- Sumários
Aula 1: 18/09/2018 Sumário (Aula Teórica): Apresentação da disciplina: Objectivos, Programa, Metodologia de Ensino e Avaliação.
Apresentação do Projecto Prático.
Sumário (Aula Prática): Apresentação do Software a usar no projecto prático.
Breve apresentação do sistema ANTLR.
Aula 2: 25/09/2018 Sumário (Aula Teórica): Gramáticas Independentes do Contexto e Análise Sintática de Programas.
Breve descrição das técnicas de Parsing Top-Down e Bottom Up.
Sumário (Aula Prática): O Sistema ANTLR: Resolução de exercícios.
Apresentação do plugin do ANTLR para o IDE IntelliJ.
Aula 3: 02/10/2018 Sumário (Aula Teórica, Prática): Continuação da realização da 1ª tarefa do projeto prático.
Aula 4: 09/10/2018 Sumário (Aula Teórica): Introdução ao Teste de Software.
Testes Unitários. Critérios de cobertura de instruções, blocos, caminhos e condições.
Sumário (Aula Prática): Testes Unitários em Java: JUnit. Análise de cobertura de testes unitátios em IntelliJ.
O Sistema Cobertura.
Aula 5: 16/10/2018 Sumário (Aula Teórica): Mutação de Software e Testes. Definição de mutantes. Testes que matam a mutação.
Sumário (Aula Prática): Análise de cobertura de testes unitátios em IntelliJ.
O Sistema Cobertura. O Sistema PIT para mutação de software e execução de testes.
Aula 6: 23/10/2018 Sumário (Aula Teórica, Prática): Geração Automática de Casos de Teste: Introdução ao sistema EvoSuite e resolução de exercícios.
Aula 7: 30/10/2018 Sumário (Aula Teórica): Teste de Propriedades. Introdução ao sistema QuickCheck.
Sumário (Aula Prática): Resolução de exercícios em QuickCheck e jUnit-QuickCheck.
Aula 8: 06/11/2018 Sumário (Aula Teórica): Geração Automática de Casos de Teste. Geração de listas e árvores em QuickCheck.
Sumário (Aula Prática): Continuação da Resolução de exercícios em QuickCheck e jUnit-QuickCheck.
Aula 9: 13/11/2018 Sumário (Aula Teórica): Localização de Falhas no Código Fonte. Introdução ao Spectrum-based Fault Localization.
Sumário (Aula Prática): Aula de acompanhamento da realização da 2a tarefa do projeto em grupo.
Aula 10: 20/11/2018 Sumário (Aula Teórica): Aula sobre Análise de Performance: Runtime, Energy and memory consumption.
Sumário (Aula Prática): O Sistema RAPL para estimar o consumo de energia.
Aula 11: 27/11/2018 Sumário (Aula Teórica): Métricas de Software. Complexidade Ciclomárica.
Sumário (Aula Prática): Introdução à ferramenta OpenClover? . Resolução da ficha de exercícios 6 sobre métricas de software.
Aula 12: 04/12/2018 Sumário (Aula Teórica): Introdução ao conceito de Bad Smells. Source code Smells: catálogo.
Sumário (Aula Prática): Apresentação da ferramenta PMD. Análise de software para detectar code smells e más práticas de programação.
Aula 13: 11/12/2018 Sumário (Aula Teórica): Refactoring.
Sumário (Aula Prática): Apresentação das funcionalidades de refactoring do IntelliJ? IDEA. Resolução da ficha de exercícios 7 sobre refactoring de programas.
Aula 14: 08/01/2019
*Sumário (Aula Teórica, Prática):*Apresentação dos projetos em grupo: grupos 2, 3, 4, 5, 8 e 10.
Aula 15: 15/01/2019 Sumário (Aula Teórica, Prática): Apresentação dos projetos em grupo: grupos 1,6,7,9 e 11.
Aula 16: 22/01/2019 Sumário (Aula Teórica, Prática): Teste Individual Aula Extra: 24/01/2019 (14:00-16:00)Sumário (Aula Teórica, Prática): Visita à Primavera Sw.
Aula 17: 29/01/2019 Sumário (Aula Teórica, Prática): Exame
8- Bibliografia
Introduction to Software Testing
J. Offutt and P. Amman
Cambridge University Press, 2008
14 Jun - VF:
O exame de VF realiza-se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12.
Os alunos deverão trazer os seus computadores pessoais com o software utilizado nas aulas instalado. É permitida a consulta da documentação na parte laboratorial do exame.
14 Jun - VF:
As notas dos projecto e notas finais foram lançadas no Blackboard.
11 Jun - VF:
As notas do 2º teste foram lançadas no Blackboard.
3 Jun - VF:
A apresentação dos projectos realiza-se no dia 12 de Junho (4º feira), às 9:00, na sala 1.10 do DI.
As apresentações são de 15 min. + 5 min. para perguntas.
Todos os alunos deverão estar presentes na sessão.
Os relatórios deverão ser entregues por email até ao dia 10 de Junho.
27 Mai - VF:
O 2º teste de VF realiza-se na próxima 5ª feira, 30 de Maio, às 14:00, na sala E7 1.10.
Os alunos deverão trazer os seus computadores pessoais com o sistemas Frama-C e CBMC instalados. É permitida a consulta da documentação.
16 Abr - VF: As notas do 1º teste foram lançadas no Blackboard.
16 Abr - VF:
A distribuição dos projectos por grupos já está disponível na página de VF.
4 Abr - VF: Os temas dos projectos estão disponíveis. Por favor, comuniquem as vossas escolhas dos projectos a mjf@di.uminho.pt até 15-Abr.
26 Fev - A Workshop ClearSy terá lugar 4ª-feira 6-Mar, às 14h30. Estejam atentos a mais informações. Até lá, recomenda-se que vejam este video.
10 Fev - LEI: a quem estiver interessado - por favor comuniquem as vossas escolhas dos projectos em LEI a jno@di.uminho.pt até 21-Fev.
10 Fev - CSI: as notas após o exame de recurso foram lançadas na página de CSI.
31 Jan - VF: As aulas de Verificação Formal começam a 14-Fev.
29 Jan - Informa-se que o exame de recurso de CSI foi adiado para dia 6-Fev, às 15h00, na sala 0.05 do DI.
29 Jan - EM: as notas do exame foram lançadas no blackboard da disciplina.
28 Jan - O enunciado do teste de CSI tem agora a correcção proposta.
28 Jan - A Workshop ClearSy de que se falou nas aulas está prevista para 6-Mar (em não Fevereiro como arradamente se referiu). Será conduzida por Thierry Lecomte, especialista em uso de MFs na indústria dos transportes.
27 Jan - CSI: as notas à data do teste foram lançadas na página de CSI.
22 Jan - EM: as notas finais da época normal foram lançadas no blackboard da disciplina. (correção parcial na wiki)
16 Jan - CSI: o teste de CSI de amanhã decorrerá na sala 0.05 do DI.
15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina.
11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.
9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.
30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.
21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.
13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).
8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.
28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.
24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.
24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.
14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.
8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.
5 Nov - CSI: há novo material pedagógico na página CSI.
25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.
21 Out - CSI: ver exemplos Alloy das aulas na página CSI.
02 Out - CSI: preparação para as aulas: ver sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')
15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.
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.
Bibliografia / Bibliography
J.N. Oliveira. Program Design by Calculation. Informatics Department, University of Minho. The chapters that matter for this course in this academic year are the 5th ( 1M), 6th ( 101K) and 7th ( 433K).
NB: poderá haver trocas de horário entre CSI e EM de acordo com necessidades de serviço dos docentes das duas disciplinas.
Alunos
Afonso Rafael Carvalho Sousa
A74196
MiEI
Alexandre Miguel Costa Dias
A78425
MiEI
Armando João Isaias Ferreira dos Santos
A77628
MiEI
Artur Queiroz
PG38014
MMC
Diogo Manuel Macedo e Silva
A79021
MiEI
Francisco Fernando Vilela Araújo
A79821
MiEI
Fábio Rafael Pereira Araújo
A78508
MiEI
Gerson Benjamim Hungulu
PG35957
MMC
Gonçalo Medeiros São Pedro Raposo
A77211
MiEI
Gonçalo Nuno Esteves Duarte
A77508
MiEI
Joana Fernandes Cunha
PG38929
MEI
Jorge Fernando Alves da Cruz
A78895
MiEI
José Carlos do Vale e Sousa
A74678
MiEI
João Manuel da Silva Gomes Fernandes
PG38930
MEI
Nelson Loureiro
PG37020
MMC
Patrícia Filipa Bouça Barreira
A79007
MiEI
Pedro Faria Durães da Silva
A78434
MiEI
Pedro Henrique Moreira Gomes Fernandes
A77377
MiEI
Pedro Miguel Gomes da Silva
PG38935
MEI
Ricardo Guerra Leal
A75411
MiEI
Tiago André Araújo Monteiro
A78961
MiEI
Programa resumido
Introdução aos métodos formais e seu papel na programação. Verificação e cálculo de soluções informáticas. Problemas e sistemas de informação para os resolver. Modelos e seu papel na concepção de soluções. Importância da abstracção na captação de requisitos. Limites da tipagem estática. Papel das relações binárias na modelação formal. Bases de dados seguindo o modelo 'key-value pair'. Taxonomia e álgebra das relações binárias. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy. Demonstração de corrrecção usando álgebra relacional. Noção formal de contrato. Pré-condições mais fracas. Lógica de Hoare em formato relacional.
Regime de avaliação
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 60%.
Formulário CSI: ( 137K) - Leis do cálculo relacional básico.
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).
Script 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
Plano de estudos do MEI - em curso, enunciado: (PDF); modelo Alloy com os quatro invariantes.
Atendimento electrónico (FAQs)
Q01 - Em b ⊥ a ≡ TRUE (página 170 dos apontamentos não devia ser b ⊤ a ≡ TRUE?R: É uma gralha, obrigado por informar. Aparecerá corrigida na próxima versão desse capítulo. Agradece-se a comunicação de outras gralhas!
Q02 - Tenho uma dúvida na primeira questão do mini teste de 7 de Dezembro 2017. Na cláusula 3, o professor na resolução tem V :E ← V, não deveria ser V :E ← P ?R: É também uma gralha, que acabo de corrigir. Obrigado por informar.
Q03 - Tentei resolver o exercício 5.45 por igualdade indirecta e não consegui. Muito provavelmente tenho que utilizar a (5.154) mas não consigo ver como.R: A igualdade c◦ ·(⊤ − c) = ⊥ é equivalente e 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⇒⊥ = ⊥.
Q04 - No exercico 5.24 aplico a definição de injectividade de uma relação seguido da definição de kernel à interseção de R com S, chegando ao ponto (R ∩ S)º . (R ∩ S) contido na identidade. Não sei como hei-de desenvolver o resto da expressão visto que não existe nenhuma fórmula para a composição de interseções.R: Este é um exemplo em que regras de monotonia ou "thumb rules" ajudam. Veja, por exemplo, como a regra (5.82) o pode ajudar a resolver o exercício.
Q05 - No exercício 5.26 não sei como é que hei-de provar que (⊤.) é um closure operator. Qual é a estratégia?R: Em (5.97) substitua ⊤ = !º.! e depois use "shunting" e (5.96).
-- JoseNunoOliveira - 15 Sep 2018
O Sistema Europeu de Gestão de Tráfego Ferroviário (ERTMS, European Rail Traffic Management System) é um conjunto de padrões que visa garantir a interoperabilidade de linhas ferroviárias na União Europeia. O seu componente de sinalização e controlo, o Sistema Europeu de Controlo de Comboios (ETCS, European Train Control System), estabelece vários níveis de conformidade com o padrão, dependendo do nível de tecnologia já implementado nas linhas e nos comboios. O Nível 3 assume que os comboios estão em comunicação constante com o sistema de controlo, a transmitir informação sobre a sua posição e integridade. Visto na prática estes sistemas ainda não serem totalmente viáveis, o Nível 3 Híbrido assume ainda a existência de sensores físicos na linha que detectam a presença de carruagens, e permitem colmatar falhas nos sistemas de deteção e comunicação.
O objetivo deste trabalho é modelar, especificar e verificar, em NuSMV, parte do conceito Nível 3 Híbrido do ERTMS/ETCS. Para tal devem basear-se no seguinte documento introdutório, assim como na especificação completa, nomeadamente na máquina de estados presente na Secção 5 e nos cenários operacionais do Anexo A. As componentes do conceito a modelar, assim como o nível de detalhe, ficam ao critério de cada grupo. Para simplificar o processo, o modelo deve representar apenas uma configuração da linha, no máximo tão complexa quanto a dos cenários operacionais do Anexo A do documento (9 blocos virtuais).
Os grupos (de 2 elementos) deverão entregar por email o trabalho até à data limite de 11-Nov-2018 (um ficheiro zip com todos os modelos desenvolvidos, devidamente comentados).
Enunciado do Trabalho 2 sobre Alloy
Uma tabelas de hash distribuída (DHT) é um sistema distribuído descentralizado que disponibiliza as funcionalidades de uma tabela de hash. Pares (chave, valor) estão distribuídos pelos vários nós, e o algoritmo de lookup garante que o valor associado a uma chave pode ser encontrado eficientemente. Para tal, algumas DHT organizam os nós numa estrutura em anel em que o identificador atribuído a cada nó orienta a pesquisa. No entanto, isto requer que a rede inevitavelmente estabilize num anel quando nós entram ou abandonam a rede. Um desses protocolos é o Chord, que foi previamente validado em Alloy. Outra alternativa é o Pastry, que foi validado previamente em TLA+, uma outra linguagem de especificação com um model checker associado.
Os grupos de trabalho devem estudar o artigo sobre a análise do Pastry 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 TLA+, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é analisar o Pastry usando Alloy em vez de TLA+. Se necessário, mas não obrigatoriamente, podem usar a especificação do Chord em Alloy como inspiração. O nível de detalhe a atingir, assim como a escolha do idioma de Alloy dinâmico, fica à consideração de cada grupo. Finalmente, os grupos devem também desenvolver um theme que facilite a compreensão das instâncias.
Os grupos deveram entregar por email o trabalho até à data limite de 20-Jan-2018 (um modelo Alloy, devidamente comentado, e o respectivo theme).
Final evaluation by industrial partners: our Skype-ID: uminho-di-a1
Project descriptions
Project 1 - CLAV - Public Information Classification and Evaluation: formal model specification (J.C. Ramalho)
CLAV is a platform being developed by DI/UM with the partnership and ordered by the Direção Geral do Livro, Arquivos e Bibliotecas (DGLAB) which aims the classification and evaluation of all documents that move around and across portuguese public institutions. One view, already visible, of the project is the so called Lista Consolidada, which is a comprehensive catalog of all administrative processes ocurring in Portuguese public institutions. The first version is available online. For further information contact the author. There are several articles and presentations about this subject. Currently, the model is specified in OWL ("Ontology Web Language"), but suffered several changes during the last year and there was no time to study the impact of those changes in the model's pre-conditions and invariants. In this project we want: (a) to formally specify the model from scratch; (b) to load the available information onto the new model; (c) to specify pre-conditions and invariants; (d) to report errors.
Project 2 - Relational algebra for data processing using strongly typed FP (J.P. Magalhães, Standard Chartered Bank, Singapore)
Relational algebra is a powerful and versatile tool for data processing. Previous work on adding static types to a relational algebra library has turned "reasoning and proving properties of programs" into simply "typechecking". However, we are often concerned about more than just the type of a relation; we might care about the keys, or the size of the relation, for example. A common use case is to process a large relation until it contains a single row with the desired answer, but currently we cannot statically express the constraint that the relation has a single row. This project looks at extending Augustsson and Ågren's earlier work to deal with such constraints (and possibly others).
Project 4 - Analysis of connectors in Alloy (Nuno Macedo, José Proença)
Reo is a language to specify how software components interact with each other.
Reo programs are called connectors - the formal semantics of these are based on transition systems that quickly become huge. The best existing approach to verify properties of such connectors rely on an external model checker based on process algebra, mCRL2, which does not cope well with (infinitely) large state spaces.
Alloy is a high-level specification language with support for automatic model finding. The language, based on relational logic, is simple and flexible, allowing the declarative specification of systems with variable configurations and alternative behaviours. Unlike in mCRL2, an Alloy specification does not explicitly describe the transition system, making it better suited to abstract away certain concepts, such as time, data, or variability.
The key scientific goal is to understand and extend the approach to model connectors with Alloy by Khosrav et al., e.g., introducing notions of time or variability.
* https://pdfs.semanticscholar.org/c1d0/78be0aa0d88baf12501668c32e2dcda8ede1.pdf
The key technical goal is to extend the ReoLive tools with support for Alloy, similar to how it is currently done for mCRL2, which will involve learning basics of Scala and JavaScript.
* https://reolanguage.github.io/ReoLive/snapshot/
This theme is proposed for MMC students. It consists in carefully studying and presenting a recent paper on this topic (The Simple Essence of Automatic Differentiation by C. Elliott, POPL 2019) including some experimentation with the library described there. A second objective is to see how it could be applied in the context of typed neural networks. There is also a video:.
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).
NB: poderá haver trocas de horário entre VF e AC de acordo com necessidades de serviço dos docentes das duas disciplinas.
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%)
Datas
1º teste: 4 de Abril (9:00)
2º teste: 30 de Maio (14:00)
Projecto
Relatório: 10 de Junho
Apresentação: 12 de Junho (9:00)
Exame de recurso: 19 Junho (14:00)
Projectos
Lean
“Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.”
Tratando-se de uma ferramenta de prova inovadora, e não de um verificador de programas, espera-se:
uma descrição geral da ferramenta e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.
Isabelle
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
Tratando-se de uma ferramenta de prova, e não de um verificador de programas, espera-se:
uma descrição geral da ferramenta e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.
Coq
"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs."
Tratando-se de uma ferramenta de prova que já foi abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
desenvolvimento de um caso de estudo que envolva a formalização em Coq de um pequeno problema;
consideração de alguns tópicos avançados, não abordados nas aulas (por exemplo, definição de tácticas automáticas);
experimentação com a ferramenta QuickChick: Randomized Property-Based Testing Plugin for Coq.
Why3
"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories and basic programming data structures. A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 can be easily extended with support for new theorem provers. Why3 can be used as a software library, through an OCaml API."
Tratando-se de uma ferramenta já abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
desenvolvimento de um caso de estudo que envolva a formalização em Why3 de um pequeno problema (ver aqui);
"Boogie
is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#.
Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.
The Boogie research project is being developed at Microsoft Research."
Espera-se:
Dafny é uma ferramenta da Microsoft Research baseada numa linguagem de programação dedicada para verificação dedutiva (tal como Why3), utilizando como VCGen uma outra ferramenta da Microsoft Research, chamada Boogie.
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
O KeY é uma ferramenta de verificação dedutiva bem estabelecida que ganhou recentemente visibilidade acrescida, pelo facto de ter permitido identificar um bug em algoritmos de ordenação implementados em bibliotecas standard (Java, Python). A lógica de programas subjacente é uma lógica dinâmica, em vez da mais comum lógica de Hoare / WP calculus.
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
O VeriFast é uma ferramenta de verificação dedutiva tendo por base a lógica de programas conhecida como “separation logic”, o que, em teoria, lhe confere algumas vantagens sobre ferramentas baseadas em lógica de Hoare / WP calculus.
“VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.”
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
identificação de aspectos em que a ferramenta suplanta as estudadas, graças à utilização de “separation logic”;
“Viper (Verification Infrastructure for Permission-based Reasoning) is a suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages, via translations into the Viper language.
The Viper toolchain is designed to make it easy to implement verification techniques for programs with persistent mutable state (including concurrent programs), providing native support for reasoning about the program state using method permissions or ownership, e.g. in the style of separation logic. New verification techniques can be implemented directly as translations to the Viper language, using either of the verifiers provided.” Trata-se de uma proposta completa, baseada numa linguagem intermédia, front-ends e back-ends. São disponibilizados dois back-ends, um dos quais recorre ao Boogie.
Espera-se naturalmente uma descrição geral da toolset e princípios subjacentes, abordando:
uma comparação entre a linguagem intermédia dedicada Wiper e a linguagem WhyML do Why3;
comparação entre Viper e Why3, trabalhando directamente sobre as respectivas linguagens dedicadas;
possível demonstração da utilização do toolset, incluindo um front-end para uma qualquer linguagem real de alto nível.
SMACK
“SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations. (…) Currently, SMACK leverages the Boogie and Corral verifiers.”
Trata-se de uma ferramenta para a verificação de código C, mas que apenas traduz para BoogiePL, sendo depois necessário utilizar uma das ferramentas referidas como back-end. O grupo deve começar por escolher uma das ferramentas; o trabalho diz respeito ao toolset completo, compreendendo o SMACK e a ferramenta (VCGen) escolhida.
Espera-se:
uma descrição geral da toolset e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização de outras ferramentas existentes para a verificação de código C;
comparação com as ferramentas similares estudadas na UC (WP / Frama-C).
TWiki's Education/MFES1819 webThe Education/MFES1819 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819Copyright 2020 by contributing authors2020-10-19T10:41:26ZWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebHome2020-10-19T10:41:26ZBem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)JoseNunoOliveiraCSIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/CSI2020-10-17T09:08:19ZUC2 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)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Avisos2020-10-17T08:50:29Z14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ... (last changed by JoseNunoOliveira)JoseNunoOliveiraVFhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/VF2020-05-07T13:52:23ZUC3 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/MFES1819/EM2020-01-08T17:23:29ZEspecificação e Modelação Docente / Horário Docente Foto Horário Sala Moreira Macedo 5a feira, 9h 12h Sala E7 1.10 NB: poderá haver ... (last changed by NunoMacedo)NunoMacedoEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EquipaDocente2019-05-20T14:04:16ZEquipa docente Soares Barbosa João Frade Moreira Macedo Nuno Oliveira Alexandre Saraiva JoseNunoOliveira ... (last changed by JoseNunoOliveira)JoseNunoOliveiraLEIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/LEI2019-05-02T11:07:22ZCohesive 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/MFES1819/WebSideBar2019-04-18T16:25:55ZTó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)JoseNunoOliveiraATShttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/ATS2019-02-15T11:06:28ZAnálise e Teste de Software Finais Teste Projeto Recurso Exame de Recurso 1 Docentes João Saraiva (homepage) Aula Teórica: 3a feira, 14:00 15:00 ... (last changed by JoaoSaraiva)JoaoSaraivaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Calendario2018-10-04T17:00:35ZCalendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 15 Sep 2018 (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebPreferences2018-09-25T22:35:13ZEducation/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaAChttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/AC2018-09-15T12:03:56ZUC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1819 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/MFES1819/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunhaWebCsshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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/MFES1819/WebTopBar2007-02-13T14:43:04Z (last changed by AlcinoCunha)AlcinoCunha
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ...
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ...
Bem vindo à página da edição de 2018/19 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.
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ...
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ...
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 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 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/MFES1819 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/MFES1819.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 (2018/2019)
Set SITEMAPUSETO = Mestrado Integrado em Engenharia Informática - MFES 2018/2019
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/MFES1819 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/MFES1819
The Education/MFES1819 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/MFES1819
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819
/twiki/pub/Main/LocalLogos/um_eengP.jpgWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebHome
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)2020-10-19T10:41:26ZJoseNunoOliveiraCSI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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-10-17T09:08:19ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Avisos
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ... (last changed by JoseNunoOliveira)2020-10-17T08:50:29ZJoseNunoOliveiraVF
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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-07T13:52:23ZMariaJoaoFradeEM
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EM
Especificação e Modelação Docente / Horário Docente Foto Horário Sala Moreira Macedo 5a feira, 9h 12h Sala E7 1.10 NB: poderá haver ... (last changed by NunoMacedo)2020-01-08T17:23:29ZNunoMacedoEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EquipaDocente
Equipa docente Soares Barbosa João Frade Moreira Macedo Nuno Oliveira Alexandre Saraiva JoseNunoOliveira ... (last changed by JoseNunoOliveira)2019-05-20T14:04:16ZJoseNunoOliveiraLEI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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)2019-05-02T11:07:22ZJoseNunoOliveiraWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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)2019-04-18T16:25:55ZJoseNunoOliveiraATS
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/ATS
Análise e Teste de Software Finais Teste Projeto Recurso Exame de Recurso 1 Docentes João Saraiva (homepage) Aula Teórica: 3a feira, 14:00 15:00 ... (last changed by JoaoSaraiva)2019-02-15T11:06:28ZJoaoSaraivaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Calendario
Calendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 15 Sep 2018 (last changed by JoseNunoOliveira)2018-10-04T17:00:35ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebPreferences
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ... (last changed by JoseBacelarAlmeida)2018-09-25T22:35:13ZJoseBacelarAlmeidaAC
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/AC
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ... (last changed by JoseNunoOliveira)2018-09-15T12:03:56ZJoseNunoOliveiraWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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/MFES1819/WebTopBar
(last changed by AlcinoCunha)2007-02-13T14:43:04ZAlcinoCunhaWebLeftBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebLeftBar
Apresentação Sumários Projectos Material (last changed by AlcinoCunha)2007-02-13T10:35:33ZAlcinoCunha
Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos.
A página oficial da cadeira encontrar-se-á em http://arca.di.uminho.pt/ac-1819.
A avaliação dos alunos é feita tendo em conta três componentes:
Nota do Teste individual (NT)
Nota do Projecto em grupo (NP)
Avaliação Contínua (AC)
de acordo com a fórmula:
nota final = 0.45 * NT + 0.45 * NP + 0.1 * AC
Nas componentes NT e NP é obrigatório o aluno ter uma nota mínima de 8 valores.
7- Sumários
Aula 1: 18/09/2018 Sumário (Aula Teórica): Apresentação da disciplina: Objectivos, Programa, Metodologia de Ensino e Avaliação.
Apresentação do Projecto Prático.
Sumário (Aula Prática): Apresentação do Software a usar no projecto prático.
Breve apresentação do sistema ANTLR.
Aula 2: 25/09/2018 Sumário (Aula Teórica): Gramáticas Independentes do Contexto e Análise Sintática de Programas.
Breve descrição das técnicas de Parsing Top-Down e Bottom Up.
Sumário (Aula Prática): O Sistema ANTLR: Resolução de exercícios.
Apresentação do plugin do ANTLR para o IDE IntelliJ.
Aula 3: 02/10/2018 Sumário (Aula Teórica, Prática): Continuação da realização da 1ª tarefa do projeto prático.
Aula 4: 09/10/2018 Sumário (Aula Teórica): Introdução ao Teste de Software.
Testes Unitários. Critérios de cobertura de instruções, blocos, caminhos e condições.
Sumário (Aula Prática): Testes Unitários em Java: JUnit. Análise de cobertura de testes unitátios em IntelliJ.
O Sistema Cobertura.
Aula 5: 16/10/2018 Sumário (Aula Teórica): Mutação de Software e Testes. Definição de mutantes. Testes que matam a mutação.
Sumário (Aula Prática): Análise de cobertura de testes unitátios em IntelliJ.
O Sistema Cobertura. O Sistema PIT para mutação de software e execução de testes.
Aula 6: 23/10/2018 Sumário (Aula Teórica, Prática): Geração Automática de Casos de Teste: Introdução ao sistema EvoSuite e resolução de exercícios.
Aula 7: 30/10/2018 Sumário (Aula Teórica): Teste de Propriedades. Introdução ao sistema QuickCheck.
Sumário (Aula Prática): Resolução de exercícios em QuickCheck e jUnit-QuickCheck.
Aula 8: 06/11/2018 Sumário (Aula Teórica): Geração Automática de Casos de Teste. Geração de listas e árvores em QuickCheck.
Sumário (Aula Prática): Continuação da Resolução de exercícios em QuickCheck e jUnit-QuickCheck.
Aula 9: 13/11/2018 Sumário (Aula Teórica): Localização de Falhas no Código Fonte. Introdução ao Spectrum-based Fault Localization.
Sumário (Aula Prática): Aula de acompanhamento da realização da 2a tarefa do projeto em grupo.
Aula 10: 20/11/2018 Sumário (Aula Teórica): Aula sobre Análise de Performance: Runtime, Energy and memory consumption.
Sumário (Aula Prática): O Sistema RAPL para estimar o consumo de energia.
Aula 11: 27/11/2018 Sumário (Aula Teórica): Métricas de Software. Complexidade Ciclomárica.
Sumário (Aula Prática): Introdução à ferramenta OpenClover? . Resolução da ficha de exercícios 6 sobre métricas de software.
Aula 12: 04/12/2018 Sumário (Aula Teórica): Introdução ao conceito de Bad Smells. Source code Smells: catálogo.
Sumário (Aula Prática): Apresentação da ferramenta PMD. Análise de software para detectar code smells e más práticas de programação.
Aula 13: 11/12/2018 Sumário (Aula Teórica): Refactoring.
Sumário (Aula Prática): Apresentação das funcionalidades de refactoring do IntelliJ? IDEA. Resolução da ficha de exercícios 7 sobre refactoring de programas.
Aula 14: 08/01/2019
*Sumário (Aula Teórica, Prática):*Apresentação dos projetos em grupo: grupos 2, 3, 4, 5, 8 e 10.
Aula 15: 15/01/2019 Sumário (Aula Teórica, Prática): Apresentação dos projetos em grupo: grupos 1,6,7,9 e 11.
Aula 16: 22/01/2019 Sumário (Aula Teórica, Prática): Teste Individual Aula Extra: 24/01/2019 (14:00-16:00)Sumário (Aula Teórica, Prática): Visita à Primavera Sw.
Aula 17: 29/01/2019 Sumário (Aula Teórica, Prática): Exame
8- Bibliografia
Introduction to Software Testing
J. Offutt and P. Amman
Cambridge University Press, 2008
14 Jun - VF:
O exame de VF realiza-se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12.
Os alunos deverão trazer os seus computadores pessoais com o software utilizado nas aulas instalado. É permitida a consulta da documentação na parte laboratorial do exame.
14 Jun - VF:
As notas dos projecto e notas finais foram lançadas no Blackboard.
11 Jun - VF:
As notas do 2º teste foram lançadas no Blackboard.
3 Jun - VF:
A apresentação dos projectos realiza-se no dia 12 de Junho (4º feira), às 9:00, na sala 1.10 do DI.
As apresentações são de 15 min. + 5 min. para perguntas.
Todos os alunos deverão estar presentes na sessão.
Os relatórios deverão ser entregues por email até ao dia 10 de Junho.
27 Mai - VF:
O 2º teste de VF realiza-se na próxima 5ª feira, 30 de Maio, às 14:00, na sala E7 1.10.
Os alunos deverão trazer os seus computadores pessoais com o sistemas Frama-C e CBMC instalados. É permitida a consulta da documentação.
16 Abr - VF: As notas do 1º teste foram lançadas no Blackboard.
16 Abr - VF:
A distribuição dos projectos por grupos já está disponível na página de VF.
4 Abr - VF: Os temas dos projectos estão disponíveis. Por favor, comuniquem as vossas escolhas dos projectos a mjf@di.uminho.pt até 15-Abr.
26 Fev - A Workshop ClearSy terá lugar 4ª-feira 6-Mar, às 14h30. Estejam atentos a mais informações. Até lá, recomenda-se que vejam este video.
10 Fev - LEI: a quem estiver interessado - por favor comuniquem as vossas escolhas dos projectos em LEI a jno@di.uminho.pt até 21-Fev.
10 Fev - CSI: as notas após o exame de recurso foram lançadas na página de CSI.
31 Jan - VF: As aulas de Verificação Formal começam a 14-Fev.
29 Jan - Informa-se que o exame de recurso de CSI foi adiado para dia 6-Fev, às 15h00, na sala 0.05 do DI.
29 Jan - EM: as notas do exame foram lançadas no blackboard da disciplina.
28 Jan - O enunciado do teste de CSI tem agora a correcção proposta.
28 Jan - A Workshop ClearSy de que se falou nas aulas está prevista para 6-Mar (em não Fevereiro como arradamente se referiu). Será conduzida por Thierry Lecomte, especialista em uso de MFs na indústria dos transportes.
27 Jan - CSI: as notas à data do teste foram lançadas na página de CSI.
22 Jan - EM: as notas finais da época normal foram lançadas no blackboard da disciplina. (correção parcial na wiki)
16 Jan - CSI: o teste de CSI de amanhã decorrerá na sala 0.05 do DI.
15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina.
11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.
9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.
30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.
21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.
13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).
8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.
28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.
24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.
24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.
14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.
8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.
5 Nov - CSI: há novo material pedagógico na página CSI.
25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.
21 Out - CSI: ver exemplos Alloy das aulas na página CSI.
02 Out - CSI: preparação para as aulas: ver sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')
15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.
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.
Bibliografia / Bibliography
J.N. Oliveira. Program Design by Calculation. Informatics Department, University of Minho. The chapters that matter for this course in this academic year are the 5th ( 1M), 6th ( 101K) and 7th ( 433K).
NB: poderá haver trocas de horário entre CSI e EM de acordo com necessidades de serviço dos docentes das duas disciplinas.
Alunos
Afonso Rafael Carvalho Sousa
A74196
MiEI
Alexandre Miguel Costa Dias
A78425
MiEI
Armando João Isaias Ferreira dos Santos
A77628
MiEI
Artur Queiroz
PG38014
MMC
Diogo Manuel Macedo e Silva
A79021
MiEI
Francisco Fernando Vilela Araújo
A79821
MiEI
Fábio Rafael Pereira Araújo
A78508
MiEI
Gerson Benjamim Hungulu
PG35957
MMC
Gonçalo Medeiros São Pedro Raposo
A77211
MiEI
Gonçalo Nuno Esteves Duarte
A77508
MiEI
Joana Fernandes Cunha
PG38929
MEI
Jorge Fernando Alves da Cruz
A78895
MiEI
José Carlos do Vale e Sousa
A74678
MiEI
João Manuel da Silva Gomes Fernandes
PG38930
MEI
Nelson Loureiro
PG37020
MMC
Patrícia Filipa Bouça Barreira
A79007
MiEI
Pedro Faria Durães da Silva
A78434
MiEI
Pedro Henrique Moreira Gomes Fernandes
A77377
MiEI
Pedro Miguel Gomes da Silva
PG38935
MEI
Ricardo Guerra Leal
A75411
MiEI
Tiago André Araújo Monteiro
A78961
MiEI
Programa resumido
Introdução aos métodos formais e seu papel na programação. Verificação e cálculo de soluções informáticas. Problemas e sistemas de informação para os resolver. Modelos e seu papel na concepção de soluções. Importância da abstracção na captação de requisitos. Limites da tipagem estática. Papel das relações binárias na modelação formal. Bases de dados seguindo o modelo 'key-value pair'. Taxonomia e álgebra das relações binárias. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy. Demonstração de corrrecção usando álgebra relacional. Noção formal de contrato. Pré-condições mais fracas. Lógica de Hoare em formato relacional.
Regime de avaliação
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 60%.
Formulário CSI: ( 137K) - Leis do cálculo relacional básico.
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).
Script 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
Plano de estudos do MEI - em curso, enunciado: (PDF); modelo Alloy com os quatro invariantes.
Atendimento electrónico (FAQs)
Q01 - Em b ⊥ a ≡ TRUE (página 170 dos apontamentos não devia ser b ⊤ a ≡ TRUE?R: É uma gralha, obrigado por informar. Aparecerá corrigida na próxima versão desse capítulo. Agradece-se a comunicação de outras gralhas!
Q02 - Tenho uma dúvida na primeira questão do mini teste de 7 de Dezembro 2017. Na cláusula 3, o professor na resolução tem V :E ← V, não deveria ser V :E ← P ?R: É também uma gralha, que acabo de corrigir. Obrigado por informar.
Q03 - Tentei resolver o exercício 5.45 por igualdade indirecta e não consegui. Muito provavelmente tenho que utilizar a (5.154) mas não consigo ver como.R: A igualdade c◦ ·(⊤ − c) = ⊥ é equivalente e 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⇒⊥ = ⊥.
Q04 - No exercico 5.24 aplico a definição de injectividade de uma relação seguido da definição de kernel à interseção de R com S, chegando ao ponto (R ∩ S)º . (R ∩ S) contido na identidade. Não sei como hei-de desenvolver o resto da expressão visto que não existe nenhuma fórmula para a composição de interseções.R: Este é um exemplo em que regras de monotonia ou "thumb rules" ajudam. Veja, por exemplo, como a regra (5.82) o pode ajudar a resolver o exercício.
Q05 - No exercício 5.26 não sei como é que hei-de provar que (⊤.) é um closure operator. Qual é a estratégia?R: Em (5.97) substitua ⊤ = !º.! e depois use "shunting" e (5.96).
-- JoseNunoOliveira - 15 Sep 2018
O Sistema Europeu de Gestão de Tráfego Ferroviário (ERTMS, European Rail Traffic Management System) é um conjunto de padrões que visa garantir a interoperabilidade de linhas ferroviárias na União Europeia. O seu componente de sinalização e controlo, o Sistema Europeu de Controlo de Comboios (ETCS, European Train Control System), estabelece vários níveis de conformidade com o padrão, dependendo do nível de tecnologia já implementado nas linhas e nos comboios. O Nível 3 assume que os comboios estão em comunicação constante com o sistema de controlo, a transmitir informação sobre a sua posição e integridade. Visto na prática estes sistemas ainda não serem totalmente viáveis, o Nível 3 Híbrido assume ainda a existência de sensores físicos na linha que detectam a presença de carruagens, e permitem colmatar falhas nos sistemas de deteção e comunicação.
O objetivo deste trabalho é modelar, especificar e verificar, em NuSMV, parte do conceito Nível 3 Híbrido do ERTMS/ETCS. Para tal devem basear-se no seguinte documento introdutório, assim como na especificação completa, nomeadamente na máquina de estados presente na Secção 5 e nos cenários operacionais do Anexo A. As componentes do conceito a modelar, assim como o nível de detalhe, ficam ao critério de cada grupo. Para simplificar o processo, o modelo deve representar apenas uma configuração da linha, no máximo tão complexa quanto a dos cenários operacionais do Anexo A do documento (9 blocos virtuais).
Os grupos (de 2 elementos) deverão entregar por email o trabalho até à data limite de 11-Nov-2018 (um ficheiro zip com todos os modelos desenvolvidos, devidamente comentados).
Enunciado do Trabalho 2 sobre Alloy
Uma tabelas de hash distribuída (DHT) é um sistema distribuído descentralizado que disponibiliza as funcionalidades de uma tabela de hash. Pares (chave, valor) estão distribuídos pelos vários nós, e o algoritmo de lookup garante que o valor associado a uma chave pode ser encontrado eficientemente. Para tal, algumas DHT organizam os nós numa estrutura em anel em que o identificador atribuído a cada nó orienta a pesquisa. No entanto, isto requer que a rede inevitavelmente estabilize num anel quando nós entram ou abandonam a rede. Um desses protocolos é o Chord, que foi previamente validado em Alloy. Outra alternativa é o Pastry, que foi validado previamente em TLA+, uma outra linguagem de especificação com um model checker associado.
Os grupos de trabalho devem estudar o artigo sobre a análise do Pastry 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 TLA+, mas apenas na medida do que é necessário para perceberem o artigo. O que se pretende neste trabalho é analisar o Pastry usando Alloy em vez de TLA+. Se necessário, mas não obrigatoriamente, podem usar a especificação do Chord em Alloy como inspiração. O nível de detalhe a atingir, assim como a escolha do idioma de Alloy dinâmico, fica à consideração de cada grupo. Finalmente, os grupos devem também desenvolver um theme que facilite a compreensão das instâncias.
Os grupos deveram entregar por email o trabalho até à data limite de 20-Jan-2018 (um modelo Alloy, devidamente comentado, e o respectivo theme).
Final evaluation by industrial partners: our Skype-ID: uminho-di-a1
Project descriptions
Project 1 - CLAV - Public Information Classification and Evaluation: formal model specification (J.C. Ramalho)
CLAV is a platform being developed by DI/UM with the partnership and ordered by the Direção Geral do Livro, Arquivos e Bibliotecas (DGLAB) which aims the classification and evaluation of all documents that move around and across portuguese public institutions. One view, already visible, of the project is the so called Lista Consolidada, which is a comprehensive catalog of all administrative processes ocurring in Portuguese public institutions. The first version is available online. For further information contact the author. There are several articles and presentations about this subject. Currently, the model is specified in OWL ("Ontology Web Language"), but suffered several changes during the last year and there was no time to study the impact of those changes in the model's pre-conditions and invariants. In this project we want: (a) to formally specify the model from scratch; (b) to load the available information onto the new model; (c) to specify pre-conditions and invariants; (d) to report errors.
Project 2 - Relational algebra for data processing using strongly typed FP (J.P. Magalhães, Standard Chartered Bank, Singapore)
Relational algebra is a powerful and versatile tool for data processing. Previous work on adding static types to a relational algebra library has turned "reasoning and proving properties of programs" into simply "typechecking". However, we are often concerned about more than just the type of a relation; we might care about the keys, or the size of the relation, for example. A common use case is to process a large relation until it contains a single row with the desired answer, but currently we cannot statically express the constraint that the relation has a single row. This project looks at extending Augustsson and Ågren's earlier work to deal with such constraints (and possibly others).
Project 4 - Analysis of connectors in Alloy (Nuno Macedo, José Proença)
Reo is a language to specify how software components interact with each other.
Reo programs are called connectors - the formal semantics of these are based on transition systems that quickly become huge. The best existing approach to verify properties of such connectors rely on an external model checker based on process algebra, mCRL2, which does not cope well with (infinitely) large state spaces.
Alloy is a high-level specification language with support for automatic model finding. The language, based on relational logic, is simple and flexible, allowing the declarative specification of systems with variable configurations and alternative behaviours. Unlike in mCRL2, an Alloy specification does not explicitly describe the transition system, making it better suited to abstract away certain concepts, such as time, data, or variability.
The key scientific goal is to understand and extend the approach to model connectors with Alloy by Khosrav et al., e.g., introducing notions of time or variability.
* https://pdfs.semanticscholar.org/c1d0/78be0aa0d88baf12501668c32e2dcda8ede1.pdf
The key technical goal is to extend the ReoLive tools with support for Alloy, similar to how it is currently done for mCRL2, which will involve learning basics of Scala and JavaScript.
* https://reolanguage.github.io/ReoLive/snapshot/
This theme is proposed for MMC students. It consists in carefully studying and presenting a recent paper on this topic (The Simple Essence of Automatic Differentiation by C. Elliott, POPL 2019) including some experimentation with the library described there. A second objective is to see how it could be applied in the context of typed neural networks. There is also a video:.
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).
NB: poderá haver trocas de horário entre VF e AC de acordo com necessidades de serviço dos docentes das duas disciplinas.
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%)
Datas
1º teste: 4 de Abril (9:00)
2º teste: 30 de Maio (14:00)
Projecto
Relatório: 10 de Junho
Apresentação: 12 de Junho (9:00)
Exame de recurso: 19 Junho (14:00)
Projectos
Lean
“Lean is an open source theorem prover and programming language being developed at Microsoft Research. Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.”
Tratando-se de uma ferramenta de prova inovadora, e não de um verificador de programas, espera-se:
uma descrição geral da ferramenta e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.
Isabelle
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
Tratando-se de uma ferramenta de prova, e não de um verificador de programas, espera-se:
uma descrição geral da ferramenta e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização das ferramentas existentes bem estabelecidas;
demonstração com base em exemplos abordados nesta UC, nomeadamente de provas com utilização de indução.
Coq
"Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs."
Tratando-se de uma ferramenta de prova que já foi abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
desenvolvimento de um caso de estudo que envolva a formalização em Coq de um pequeno problema;
consideração de alguns tópicos avançados, não abordados nas aulas (por exemplo, definição de tácticas automáticas);
experimentação com a ferramenta QuickChick: Randomized Property-Based Testing Plugin for Coq.
Why3
"Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories and basic programming data structures. A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 can be easily extended with support for new theorem provers. Why3 can be used as a software library, through an OCaml API."
Tratando-se de uma ferramenta já abordada nesta UC, o que se pretende com este projecto é que o grupo vá mais longe na utilização desta ferramenta.
Espera-se:
desenvolvimento de um caso de estudo que envolva a formalização em Why3 de um pequeno problema (ver aqui);
"Boogie
is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#.
Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.
The Boogie research project is being developed at Microsoft Research."
Espera-se:
Dafny é uma ferramenta da Microsoft Research baseada numa linguagem de programação dedicada para verificação dedutiva (tal como Why3), utilizando como VCGen uma outra ferramenta da Microsoft Research, chamada Boogie.
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
O KeY é uma ferramenta de verificação dedutiva bem estabelecida que ganhou recentemente visibilidade acrescida, pelo facto de ter permitido identificar um bug em algoritmos de ordenação implementados em bibliotecas standard (Java, Python). A lógica de programas subjacente é uma lógica dinâmica, em vez da mais comum lógica de Hoare / WP calculus.
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
O VeriFast é uma ferramenta de verificação dedutiva tendo por base a lógica de programas conhecida como “separation logic”, o que, em teoria, lhe confere algumas vantagens sobre ferramentas baseadas em lógica de Hoare / WP calculus.
“VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.”
Espera-se:
tutorial sobre a utilização da ferramenta;
comparação com as ferramentas similares estudadas na UC (WP e Why3);
identificação de aspectos em que a ferramenta suplanta as estudadas, graças à utilização de “separation logic”;
“Viper (Verification Infrastructure for Permission-based Reasoning) is a suite of tools developed at ETH Zurich, providing an architecture on which new verification tools and prototypes can be developed simply and quickly. It comprises a novel intermediate verification language, also named Viper, and automatic verifiers for the language, as well as example front-end tools. The Viper toolset can be used to implement verification techniques for front-end programming languages, via translations into the Viper language.
The Viper toolchain is designed to make it easy to implement verification techniques for programs with persistent mutable state (including concurrent programs), providing native support for reasoning about the program state using method permissions or ownership, e.g. in the style of separation logic. New verification techniques can be implemented directly as translations to the Viper language, using either of the verifiers provided.” Trata-se de uma proposta completa, baseada numa linguagem intermédia, front-ends e back-ends. São disponibilizados dois back-ends, um dos quais recorre ao Boogie.
Espera-se naturalmente uma descrição geral da toolset e princípios subjacentes, abordando:
uma comparação entre a linguagem intermédia dedicada Wiper e a linguagem WhyML do Why3;
comparação entre Viper e Why3, trabalhando directamente sobre as respectivas linguagens dedicadas;
possível demonstração da utilização do toolset, incluindo um front-end para uma qualquer linguagem real de alto nível.
SMACK
“SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. SMACK handles complicated feature of the C language, including dynamic memory allocation, pointer arithmetic, and bitwise operations. (…) Currently, SMACK leverages the Boogie and Corral verifiers.”
Trata-se de uma ferramenta para a verificação de código C, mas que apenas traduz para BoogiePL, sendo depois necessário utilizar uma das ferramentas referidas como back-end. O grupo deve começar por escolher uma das ferramentas; o trabalho diz respeito ao toolset completo, compreendendo o SMACK e a ferramenta (VCGen) escolhida.
Espera-se:
uma descrição geral da toolset e princípios subjacentes;
referência às vantagens que possa oferecer relativamente à utilização de outras ferramentas existentes para a verificação de código C;
comparação com as ferramentas similares estudadas na UC (WP / Frama-C).
TWiki's Education/MFES1819 webThe Education/MFES1819 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819Copyright 2020 by contributing authors2020-10-19T10:41:26ZWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebHome2020-10-19T10:41:26ZBem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)JoseNunoOliveiraCSIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/CSI2020-10-17T09:08:19ZUC2 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)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Avisos2020-10-17T08:50:29Z14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ... (last changed by JoseNunoOliveira)JoseNunoOliveiraVFhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/VF2020-05-07T13:52:23ZUC3 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/MFES1819/EM2020-01-08T17:23:29ZEspecificação e Modelação Docente / Horário Docente Foto Horário Sala Moreira Macedo 5a feira, 9h 12h Sala E7 1.10 NB: poderá haver ... (last changed by NunoMacedo)NunoMacedoEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EquipaDocente2019-05-20T14:04:16ZEquipa docente Soares Barbosa João Frade Moreira Macedo Nuno Oliveira Alexandre Saraiva JoseNunoOliveira ... (last changed by JoseNunoOliveira)JoseNunoOliveiraLEIhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/LEI2019-05-02T11:07:22ZCohesive 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/MFES1819/WebSideBar2019-04-18T16:25:55ZTó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)JoseNunoOliveiraATShttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/ATS2019-02-15T11:06:28ZAnálise e Teste de Software Finais Teste Projeto Recurso Exame de Recurso 1 Docentes João Saraiva (homepage) Aula Teórica: 3a feira, 14:00 15:00 ... (last changed by JoaoSaraiva)JoaoSaraivaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Calendario2018-10-04T17:00:35ZCalendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 15 Sep 2018 (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebPreferences2018-09-25T22:35:13ZEducation/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ... (last changed by JoseBacelarAlmeida)JoseBacelarAlmeidaAChttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/AC2018-09-15T12:03:56ZUC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1819 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/MFES1819/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunhaWebCsshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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/MFES1819/WebTopBar2007-02-13T14:43:04Z (last changed by AlcinoCunha)AlcinoCunha
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ...
Cohesive Project (Lab. EI) Material Interesting and useful slides for preparing your milestone presentations: http://research.microsoft.com/en us/um/people/simonpj ...
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ...
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ...
Bem vindo à página da edição de 2018/19 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.
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ...
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ...
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 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ...
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 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/MFES1819 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/MFES1819.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 (2018/2019)
Set SITEMAPUSETO = Mestrado Integrado em Engenharia Informática - MFES 2018/2019
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/MFES1819 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/MFES1819
The Education/MFES1819 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/MFES1819
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819
/twiki/pub/Main/LocalLogos/um_eengP.jpgWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebHome
Bem vindo ao Perfil de MFES Bem vindo à página da edição de 2018/19 do perfil de Métodos Formais em Engenharia de Software . Este perfil de especialização do conta ... (last changed by JoseNunoOliveira)2020-10-19T10:41:26ZJoseNunoOliveiraCSI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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-10-17T09:08:19ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Avisos
14 Jun VF : O exame de VF realiza se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12 . Os alunos deverão trazer os seus computadores pessoais com ... (last changed by JoseNunoOliveira)2020-10-17T08:50:29ZJoseNunoOliveiraVF
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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-07T13:52:23ZMariaJoaoFradeEM
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EM
Especificação e Modelação Docente / Horário Docente Foto Horário Sala Moreira Macedo 5a feira, 9h 12h Sala E7 1.10 NB: poderá haver ... (last changed by NunoMacedo)2020-01-08T17:23:29ZNunoMacedoEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/EquipaDocente
Equipa docente Soares Barbosa João Frade Moreira Macedo Nuno Oliveira Alexandre Saraiva JoseNunoOliveira ... (last changed by JoseNunoOliveira)2019-05-20T14:04:16ZJoseNunoOliveiraLEI
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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)2019-05-02T11:07:22ZJoseNunoOliveiraWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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)2019-04-18T16:25:55ZJoseNunoOliveiraATS
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/ATS
Análise e Teste de Software Finais Teste Projeto Recurso Exame de Recurso 1 Docentes João Saraiva (homepage) Aula Teórica: 3a feira, 14:00 15:00 ... (last changed by JoaoSaraiva)2019-02-15T11:06:28ZJoaoSaraivaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/Calendario
Calendarização / Sumários Actualização contínua no calendário: JoseNunoOliveira 15 Sep 2018 (last changed by JoseNunoOliveira)2018-10-04T17:00:35ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebPreferences
Education/MFES1819 Web Preferences The following settings are web preferences of the Education/MFES1819 web. These preferences overwrite the site level preferences ... (last changed by JoseBacelarAlmeida)2018-09-25T22:35:13ZJoseBacelarAlmeidaAC
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/AC
UC4 Arquitectura e Cálculo (2ª semestre) Este curso tem por objectivo o estudo de modelos e cálculos em arquitectura de software, com ênfase nos sistemas reactivos ... (last changed by JoseNunoOliveira)2018-09-15T12:03:56ZJoseNunoOliveiraWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/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/MFES1819/WebTopBar
(last changed by AlcinoCunha)2007-02-13T14:43:04ZAlcinoCunhaWebLeftBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1819/WebLeftBar
Apresentação Sumários Projectos Material (last changed by AlcinoCunha)2007-02-13T10:35:33ZAlcinoCunha
14 Jun - VF:
O exame de VF realiza-se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12.
Os alunos deverão trazer os seus computadores pessoais com o software utilizado nas aulas instalado. É permitida a consulta da documentação na parte laboratorial do exame.
14 Jun - VF:
As notas dos projecto e notas finais foram lançadas no Blackboard.
11 Jun - VF:
As notas do 2º teste foram lançadas no Blackboard.
3 Jun - VF:
A apresentação dos projectos realiza-se no dia 12 de Junho (4º feira), às 9:00, na sala 1.10 do DI.
As apresentações são de 15 min. + 5 min. para perguntas.
Todos os alunos deverão estar presentes na sessão.
Os relatórios deverão ser entregues por email até ao dia 10 de Junho.
27 Mai - VF:
O 2º teste de VF realiza-se na próxima 5ª feira, 30 de Maio, às 14:00, na sala E7 1.10.
Os alunos deverão trazer os seus computadores pessoais com o sistemas Frama-C e CBMC instalados. É permitida a consulta da documentação.
16 Abr - VF: As notas do 1º teste foram lançadas no Blackboard.
16 Abr - VF:
A distribuição dos projectos por grupos já está disponível na página de VF.
4 Abr - VF: Os temas dos projectos estão disponíveis. Por favor, comuniquem as vossas escolhas dos projectos a mjf@di.uminho.pt até 15-Abr.
26 Fev - A Workshop ClearSy terá lugar 4ª-feira 6-Mar, às 14h30. Estejam atentos a mais informações. Até lá, recomenda-se que vejam este video.
10 Fev - LEI: a quem estiver interessado - por favor comuniquem as vossas escolhas dos projectos em LEI a jno@di.uminho.pt até 21-Fev.
10 Fev - CSI: as notas após o exame de recurso foram lançadas na página de CSI.
31 Jan - VF: As aulas de Verificação Formal começam a 14-Fev.
29 Jan - Informa-se que o exame de recurso de CSI foi adiado para dia 6-Fev, às 15h00, na sala 0.05 do DI.
29 Jan - EM: as notas do exame foram lançadas no blackboard da disciplina.
28 Jan - O enunciado do teste de CSI tem agora a correcção proposta.
28 Jan - A Workshop ClearSy de que se falou nas aulas está prevista para 6-Mar (em não Fevereiro como arradamente se referiu). Será conduzida por Thierry Lecomte, especialista em uso de MFs na indústria dos transportes.
27 Jan - CSI: as notas à data do teste foram lançadas na página de CSI.
22 Jan - EM: as notas finais da época normal foram lançadas no blackboard da disciplina. (correção parcial na wiki)
16 Jan - CSI: o teste de CSI de amanhã decorrerá na sala 0.05 do DI.
15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina.
11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.
9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.
30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.
21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.
13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).
8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.
28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.
24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.
24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.
14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.
8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.
5 Nov - CSI: há novo material pedagógico na página CSI.
25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.
21 Out - CSI: ver exemplos Alloy das aulas na página CSI.
02 Out - CSI: preparação para as aulas: ver sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')
15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.
14 Jun - VF:
O exame de VF realiza-se no dia 19 de Junho (4ª feira), às 14:00, na sala CP2 1.12.
Os alunos deverão trazer os seus computadores pessoais com o software utilizado nas aulas instalado. É permitida a consulta da documentação na parte laboratorial do exame.
14 Jun - VF:
As notas dos projecto e notas finais foram lançadas no Blackboard.
11 Jun - VF:
As notas do 2º teste foram lançadas no Blackboard.
3 Jun - VF:
A apresentação dos projectos realiza-se no dia 12 de Junho (4º feira), às 9:00, na sala 1.10 do DI.
As apresentações são de 15 min. + 5 min. para perguntas.
Todos os alunos deverão estar presentes na sessão.
Os relatórios deverão ser entregues por email até ao dia 10 de Junho.
27 Mai - VF:
O 2º teste de VF realiza-se na próxima 5ª feira, 30 de Maio, às 14:00, na sala E7 1.10.
Os alunos deverão trazer os seus computadores pessoais com o sistemas Frama-C e CBMC instalados. É permitida a consulta da documentação.
16 Abr - VF: As notas do 1º teste foram lançadas no Blackboard.
16 Abr - VF:
A distribuição dos projectos por grupos já está disponível na página de VF.
4 Abr - VF: Os temas dos projectos estão disponíveis. Por favor, comuniquem as vossas escolhas dos projectos a mjf@di.uminho.pt até 15-Abr.
26 Fev - A Workshop ClearSy terá lugar 4ª-feira 6-Mar, às 14h30. Estejam atentos a mais informações. Até lá, recomenda-se que vejam este video.
10 Fev - LEI: a quem estiver interessado - por favor comuniquem as vossas escolhas dos projectos em LEI a jno@di.uminho.pt até 21-Fev.
10 Fev - CSI: as notas após o exame de recurso foram lançadas na página de CSI.
31 Jan - VF: As aulas de Verificação Formal começam a 14-Fev.
29 Jan - Informa-se que o exame de recurso de CSI foi adiado para dia 6-Fev, às 15h00, na sala 0.05 do DI.
29 Jan - EM: as notas do exame foram lançadas no blackboard da disciplina.
28 Jan - O enunciado do teste de CSI tem agora a correcção proposta.
28 Jan - A Workshop ClearSy de que se falou nas aulas está prevista para 6-Mar (em não Fevereiro como arradamente se referiu). Será conduzida por Thierry Lecomte, especialista em uso de MFs na indústria dos transportes.
27 Jan - CSI: as notas à data do teste foram lançadas na página de CSI.
22 Jan - EM: as notas finais da época normal foram lançadas no blackboard da disciplina. (correção parcial na wiki)
16 Jan - CSI: o teste de CSI de amanhã decorrerá na sala 0.05 do DI.
15 Jan - EM: as notas do segundo teste foram lançadas no blackboard da disciplina.
11 Jan - CSI: as notas do mini-teste foram lançadas na página de CSI.
9 Jan - EM: o teste de EM decorrerá na sala 0.05 do DI.
30 Dec - EM: as notas do TP1 e do primeiro mini-teste foram lançadas no blackboard da disciplina.
21 Dec - EM: foi lançado o enunciado do TP2 sobre Alloy na página EM. A data limite da entrega é 20-Jan.
13 Dez - O segundo teste de EM decorrerá no dia 10-Jan às 9h00 (sala a indicar). O segundo teste de CSI decorrerá no dia 17-Jan (sala e hora a confirmar).
8 Dez - Lista recente e actualizada de empresas que usam métodos formais na indústria.
28 Nov - CSI: haverá hoje uma aula de dúvidas às 16h00, na sala 1.16.
24 Nov - CSI: já está disponível o formulário na página de CSI, bem como algumas FAQs.
24 Nov - CSI: o mini-teste decorrerá às 14h00 de 29-Nov, na sala das aulas. Os alunos podem consultar (apenas) informação escrita ou impressa.
14 Nov - EM: o primeiro teste decorrerá às 9h00 na sala das aulas. Podem usar os portáteis para testar execuções no NuSMV.
8 Nov - CSI: em casa, completar os invariantes I3 e I4 do modelo Alloy do problema Plano de Estudos do MEI saído da aula de hoje material pedagógico na página CSI.
5 Nov - CSI: há novo material pedagógico na página CSI.
25 Out - EM: foi lançado o enunciado do TP1 sobre NuSMV na página EM. A data limite da entrega é 11-Nov.
21 Out - CSI: ver exemplos Alloy das aulas na página CSI.
02 Out - CSI: preparação para as aulas: ver sumários previstos e seguir as respectivas indicações nos apontamentos fornecidos na bibliografia. (Em CSI segue-se o método 'Flipped Classroom')
15 Set - Início das aulas: 20-Set, 9h00, sala E7 1.10.
1M
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.