A nota do módulo de AMT será a média pesada dos seguintes componentes:
Teste individual sobre Alloy (40%).
1 exercício sobre Linguagens de Modelação (20%).
1 exercício sobre Model Checking (20%).
1 mini-projecto sobre Qualidade e Teste de Software (20%).
Notas
Número
Nome
Alloy (0-20)
LM (0-10)
MC (0-10)
QTS (0-10)
Final (0-20)
pg22796
André Santos
14.5
8.5
10
7.5
16
pg22840
Cristiano Sousa
16.5
8.5
6
8
16
pg23205
Daniel Murta
18
9
10
8
18
Deise Santana Maia
6.5
6.5
4
7.5
10
pg22766
Fábio Sousa
9
6.5
4
0
8
pg22811
Guilherme Rodrigues
11.5
9
10
8
15
pg16334
José Miguel Magalhães
9
10
8
pg23208
José Pinheiro
8.5
6.5
7
6.5
11
pg22808
Maria João Magalhães
7
9
10
8
14
pg22815
Nuno Carvalho
11.5
8.5
6
8
14
Thiago Mendonça Ramos
8
6.5
4
7.5
10
pg22832
Tiago Guimarães
12
6.5
7
6.5
13
pg22576
Tiago Ferreira
12
6.5
8
7.5
14
pg22812
Tiago Jorge
14
9
10
8
16
pg21319
Victor Miraldo
16.5
8.5
10
7.5
17
pg22577
Xavier Pinho
7.5
6.5
8
7.5
12
Exercício sobre Linguagens de Modelação
O objectivo deste exercício é estudar uma linguagem de modelação formal alternativa ao Alloy. Este exercício será realizado em grupos. O prazo de entrega é 31 de Janeiro de 2013. Até esta data deverão submeter por email para o docente responsável:
Um modelo formal equivalente ao exemplo em Alloy atribuído ao grupo.
Um parágrafo sintetizando as maiores diferenças a nível da linguagem (sintaxe, semântica, sistema de tipos, bibliotecas, etc) entre o Alloy e a linguagem atribuída ao grupo.
Um parágrafo sintetizando o suporte que a linguagem atribuída ao grupo possui em termos de ferramentas para validação / verificação (nomeadamente, descrevendo se é possível efectuar os comandos presentes no exemplo, para verificação de consistência do modelo ou verificar uma determinada propriedade).
No artigo em que propôs o algoritmo para exclusão mútua entre 2 processos, Peterson propôs também uma generalização simples para n processos. Esta generalização garante a exclusão mútua, mas, infelizmente, não garante incondicionalmente a ausência de starvation quando n > 2. Usando o NuSMV modele este algoritmo e tente encontrar um contra-exemplo para essa propriedade.
Este exercício será realizado em grupos de dois alunos. O prazo de entrega é 31 de Janeiro de 2013. Até esta data deverão submeter por email para o docente responsável o ficheiro SMV com o modelo do algoritmo e a especificação da propriedade que origina o contra-exemplo.
Mini-projecto sobre Qualidade e Teste de Software
O objectivo deste projecto é analisar a qualidade de software de um projecto open-source de média/grande dimensão. Mais concretamente, pretende-se analisar a vertente de maintainability segundo o modelo proposto pela SIG nas seguintes publicações:
I. Heitlager, T. Kuipers, and J. Visser. A Practical Model for Measuring Maintainability, In proceedings of the 6th International Conference on the Quality of Information and Communications Technology (QUATIC 2007), pages 30-39, IEEE Computer Society Press, 2007.
Para efeitos de comparação, este ano vamos restringir-nos a projectos Apache cuja implementação seja maioritariamente feita em Java. Uma lista dos potenciais projectos pode ser encontrada em http://www.ohloh.net/orgs/apache/projects. Este mini-projecto deverá ser realizado em grupos com no máximo 3 alunos. Cada grupo deverá analisar um projecto diferente: as escolhas e constituição dos grupos serão publicados nesta página e deverão ser comunicados logo que possível ao docente responsável. O prazo de entrega é 30 de Junho de 2013. Até esta data deverão submeter por email o relatório com a análise efectuada (max 3 páginas), onde, para além da análise global, deverão também procurar identificar os componentes mais críticos e, na medida do possível, apresentar razões que justifiquem a nota obtida.
Exercício para a primeira aula (não sujeito a avaliação)
Este exercício deverá ser realizado em grupos de 3 alunos e entregue manuscrito durante a aula.
A especificação de modelos de software é um dos ingrediente essenciais desta UC. Dada a vossa formação prévia, presumo que este conceito não seja novo. Responda sucintamente às seguintes questões:
O que é um modelo?
Quais são os objectivos da modelação?
Das linguagens/formalismos que aprendeu qual pensa ser mais adequada a modelar software? Justifique.
Considere os seguintes requisitos para uma agenda eletrônica de um cliente de email (adaptado de [1]):
A agenda deve associar endereços de email a identificadores curtos mais convenientes de usar.
Nomeadamente, o utilizador deve poder criar um alias para para um determinado correspondente (um identificador único que permanece igual mesmo que o endereço de email se altere).
Deve também poder criar um grupo que agrega vários emails, alias ou outros grupos.
Dado um identificador deve ser possível consultar todos os endereços de mail a ele associados (directa ou indirectamente).
Todos os identificadores devem estar associados (directa ou indirectamente) a pelo menos um endereço de mail.
Especifique um modelo para esta aplicação usando a linguagem/formalismo que escolheu acima. Acha que o seu modelo cumpre os objectivos que indicou?
[1] Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
Síntese das soluções:
15 Jul - Exame de recurso do módulo CSI - terá lugar dia 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.
15 Jul - Publicadas as notas finais da época normal em Funcionamento6 Jul - As notas finais de AMT foram publicadas.
10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.
08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.
06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em Sumários.
06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até 3-Jul 2013.
13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.
04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.
13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).
28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).
24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.
13 Set - Criação do site.
As aulas desta UCE decorrem todas num só dia, à 5ª-feira, das 9h00-19h00 e numa só sala, o Laboratório DI 1.08. Os meios audiovisuais estão localizados na parte anterior do laboratório.
A parte posterior está ocupada com 6 Macs Core2duo 2.0GHz/2GB/250GB/ATI2400XT/20", com sistema operativo Mac OS X. Outros sistemas operativos estão disponíveis através de Vmware Fusion. Nestas máquinas encontra-se todo o software necessário à componente experimental da UCE.
Os alunos podem deixar os seus haveres no laboratório no período de almoço. Podem ainda usar os armários que estão sob as janelas para aí deixarem material de umas sessões para outras.
A entrada no laboratório está controlada por um sistema de identificação de impressão digital, estando o acesso reservado a docentes das UCEs que aí funcionam e técnicos.
Quando
A calendarização prevista para a UCE está disponível no respectivo plano.
São feitas adaptações sempre que necessário (por exemplo, aquando das milestones do Projecto Integrado (PI), sessões de docentes convidados, etc)
Regime de Avaliação
A nota final é a média pesada das notas obtidas nos diferentes módulos:
Para obter aprovação à UCE os alunos terão que ter aprovação em todos os módulos: excepcionalmente poderão ser aprovados alunos que tenham reprovado a um dos módulos teóricos (a aprovação no projecto integrado é sempre obrigatória). Quem reprovar à UCE poderá fazer um único exame de recurso que aborda a matéria dos quatro módulos e que vale 60% da nota final. O projecto integrado não tem direito a recurso.
Oportunamente serão indicados os métodos de avaliação para cada um dos módulos.
Classificações
Classificações Finais (época normal)
NB(1): Fórmula de cálculo: 0.15*CSI+0.15*AMT+0.15*PAS+0.15*VFS+0.4*PINB(2): Todas as notas estão arredondadas à unidade.
J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.
Acetatos
J.N. Oliveira. Data type invariants: starting where (static) type checking stops (31 slides) 2012.
J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (35 slides) (updated 2012)
Alcino Cunha. An introduction to Alloy. Acetatos ligeiramente desactualizados no que respeita à modelação de sistemas dinâmicos.
J.N. Oliveira. PF transform: when everything becomes a relation (57 slides) (last update: Oct-2012)
J.N. Oliveira. “Theorems for free”: a (calculational) introduction (29 slides) (last update: Nov-2012)
J.N. Oliveira. PF transform: conditions and coreflexives for ESC (35 slides)
Alcino Cunha. Alloy: Under the Hood. Acetatos sobre semântica de lógica relacional, sistema de tipos e model finding. Para quem preferir código a notação matemática, pode consultar este programa em Haskell que implementa a semântica e o sistema de tipos.
Alcino Cunha. A perspective on model checking. Acetatos sobre modelação, especificação e verificação de sistemas reactivos: estruturas de Kripke, redes de Petri, lógica temporal (LTL e CTL), verificação de modelos por enumeração exaustiva do espaço de estados e simbólica, ordered binary decision diagrams.
Instale a ferramenta de model checking NuSMV e utilize-a para resolver os seguintes exercícios:
Verifique que o algoritmo de Peterson para exclusão mútua entre 2 processos satisfaz as seguintes propriedades:
Exclusão mútua: os processos não estão simultaneamente na região crítica;
Ausência de starvation: um processo que pretenda aceder à região crítica eventualmente conseguirá;
Prioridade: o primeiro processo a requisitar o acesso à região crítica é o sempre o primeiro a aceder à dita.
As seguintes propriedades em lógica temporal não são equivalentes. Tente encontrar sistemas de transição (o mais simples possíveis) que confirmem isso:
Motivação: quando é que se pode dizer que um programa está correcto? E que teorias / estratégias / técnicas / ferramentas temos para o garantir?
Papel da abstracção e da modelação. Modelos e protótipos. Captação de requisitos e sua relação com a interpretação gramatical. Ciclo de desenvolvimento de Balzer.
Importância dos sistemas de tipos. Limites da tipagem estática. Necessidade de invariantes de tipo. Primeira obrigação de prova: preservação de um invariante.
Necessidade de pre-condições para (a) especificação implícita de funções; (b) modelar o indeterminismo da realidade; (c) modelar relações; (d) permitir liberalidade ao especificador.
Pares pre/post: satisfiabilidade. Obrigações de prova: necessidade de uma transformada para a lógica e teoria de conjuntos. Transformada PF.
Estudo do cálculo de relações binárias. Relações simples e relações co-reflexivas. Representação de conjuntos por co-reflexivas.
"Extended Static Checking" (ESC) usando a transformada-PF. Caso de estudo em verificação estática estendida: o VFS (Verified File System).
Propriedades expressas sob a forma de conecções de Galois.
Polimorfismo funcional versus ESC: tipos vistos como relações. Cálculo da relação associada a um tipo polimórfico. Teorema grátis de uma função polimórfica (ou teorema de Reynolds-Wadler).
"ESC for free'': Regras do cálculo de obrigações de prova.
Análise, Modelação e Teste
Ciclo de desenvolvimento de software com métodos formais.
O papel da abstracção na modelação formal.
Especificação e verificação formal de software: a linguagem de especificação formal Alloy.
Especificação e verificação formal de sistemas reactivos: model checking de lógica temporal.
Teste de software: teste unitário e funcional, análise de cobertura, teste orientado aos modelos, geração de testes, injecção de falhas.
Qualidade de software: métricas de software, normas de codificação e verificação de estilo.
Verificação Formal de Software
Introdução à verificação formal. Estudo de uma linguagem imperativa simples. Semântica operacional de transições dada por uma máquina abstracta. Semântica operacional estrutural. Semântica de avaliação. Propriedades e relação entre semânticas.
Lógica de Hoare. Construção de árvores de prova com base na noção de "pré-condição mais fraca". Uma arquitectura para a verificação de programas. Algoritmo VCGen.
Estudo do plugin “Jessie'' para verificação dedutiva. O VCGen genérico “Why'' e interface gráfica “Gwhy''. Sua utilização com múltiplas ferramentas de prova automática. A linguagem de anotações ACSL; verificação baseada em contratos.
Lambda calculi tipados. Lógica de Ordem Superior. Isomorfismo de Curry-Howard. Sistema de prova assistida Coq. Extracção de programas.
Processos e Arquitecturas de Software
Introdução aos sistemas reactivos. Motivação e definição base.
Fundamentos: sistemas, comportamento e coindução.
Noção de sistema de transição etiquetado e correspondente morfismo. Noção de simulação e bisimulação. Propriedades.
Modelação de processos em CCS. Sintaxe e semântica operacional. Exemplos. Bissimilaridade e equivalência estrita.
Cálculo de processos em CCS. Equivalência e igualdade observacional. Leis. O teorema da expansão. Resolução de equações.
Estudo de linguagens para descrição de arquitecturas de software: REO e ORC.
Projecto Integrado
Nestas horas lectivas os alunos realizam, em grupo, projectos propostos pelas empresas que patrocinam a UCE, previamente apresentados pelos proponentes numa workshop interna que dá início ao processo.
No decorrer do projecto há visitas dos alunos às instalações das empresas sempre que tal é conveniente.
No final do ano, o PI fecha-se com uma outra workshop em que os grupos apresentam os seus resultados aos docentes e staff das empresas (por video-conferência, se necessário), participando estes últimos também na sessão de avaliação final.
For more details about any of these proposals please contact its proponent:
(1) Enforcing model consistency with minimal repairs (Alcino Cunha)
Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models may coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Recently, we have developed the Echo framework (https://github.com/haslab/echo) to automatically enforce consistency between different models, based on the OMG bidirectional model transformation language QVT-R. Our framework is solver based (currently implemented on top of Alloy), and ensures that an update to one of the models is automatically propagated in a minimal way to the remaining ones in order to recover consistency. The main problem of this framework is efficiency: currently it only handles well models with sizes up to the hundreds of elements, which is far from the realistic model sizes required in industrial applications. The goal of this thesis is to pursue the developing of the Echo framework, and explore different techniques to increase its efficiency. Some of the techniques to consider include solver based approaches, such as MaxSat solvers (http://en.wikipedia.org/wiki/Maximum_satisfiability_problem), to speed up the generation of satisfying instances with minimal differences to a given target instance, or heurisitic techniques developed in the model repair research area, such as the one described in http://dl.acm.org/citation.cfm?id=2351707.
This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.
(2) A cookbook of bidirectional model transformations (Alcino Cunha)
Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models mays coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Bidirectional model transformation tools promise to ease this task, by enabling the user to write once and for all a specification that states how two models are to be kept consistent, and then automatically propagating updates in one model to updates in the other, in order to recover consistency according to that specification. There are many bidirectional transformation tools and languages, sometimes differing considerably in their features and expressiveness, making it difficult for a newcomer to access which is more adequate to his specific needs. The goal of this thesis is to develop a cookbook of paradigmatic bidirectional model transformation examples, deployed in different languages and tools. Besides helping software engineerings develop their own bidirectional model transformations, this cookbook will also act as a comparative survey of the existing tools and languages, helping pinpoint their similarities and idiosyncrasies in the context of concrete examples.
This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.
(3) Formal support for modeling and quantitative analysis of the reliability of safety critical systems (J.N. Oliveira)
Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. Extreme care is necessary given that a failure of the system may result in severe consequences. A rigorous analysis must consider the combination of the system behavior together with the domain assumptions and constraints of the environment where the system is to operate. Effective results should conduct to the identification of new (safety) requirements that help preventing the identified hazards and complement the initial system requirements.
The purpose of this work is to develop a strong formally supported process for the modeling and quantitative analysis of high-assurance systems. The formal support should contribute both to the safety analysis process and to the subsequent derivation of safety requirements and/or system constraints.
The work is to be based both on well-established analysis techniques such as fault propagation and novel paradigms that involve human-automation interactions and hazardous control actions.
The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.
This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.
(4) Techniques for automatic representation of requirements for critical software systems in multiple views. (Alcino Cunha)
Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. In this process, getting the requirements right is key: it is against them that the final system behavior is analyzed and verified. Errors introduced and not detected at the requirements stage propagate throughout the development and are later much more costly to correct.
The purpose of this work is to assist engineers developing and validating systems’ and software requirements, combining multiple viewpoints to their definition and analysis. Each view represents a subset of the relevant attributes of the system. Complementary views include, for example, structural, functional, behavioral, and data flow.
The goal is to develop a set of automatic bidirectional transformations between the different views in order to be able to generate, update, and keep consistent the information visible in each viewpoint.
The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.
This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.
(5) Calculating risk in component-oriented software systems using the LAoP (J.N. Oliveira)
Fault-injection exercises already undertaken in functional programs promise to scale up fault propagation calculation from stand-alone programs to architectures based on software-components. This will provide a semantically richer alternative to similar metrics produced elsewhere on the basis of call graphs and heuristic methods.
In this project we wish to experiment with injecting faults in coalgebric semantic models of component-based systems
and derive algebraic laws enabling one to reason about how faults propagate in such systems and how they could
be mitigated. From the same LAoP formalization one should obtain other quantitative (QoS) analyses of component systems just by changing the underlying (cost) semiring.
Experiments will be carried out a probabilistic extension to the monadic animation of the component algebra already used in the PAS module.
This proposal is supported by a grant of FCT project NASONI - Heterogeneous software coordination: Foundations, methods, tools(PTDC/EEI-CTP/2341/2012).
The following document contains directions for a partnership between MFES and this well-known innovative SME focusing on the embedded market. In particular, it contains themes for MSc theses to start in the following academic year:
TWiki's Education/MFES1213 webThe Education/MFES1213 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213Copyright 2020 by contributing authors2015-03-04T13:34:19ZMaterialhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Material2015-03-04T13:34:19ZMaterial disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ... (last changed by MariaJoaoFrade)MariaJoaoFradeWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebSideBar2014-09-20T21:41:44ZTópicos Benvindo a MFES Docentes Contacto Sumários principal Alunos Funcionamento Programa Material Projecto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebHome2013-09-11T12:03:49ZBem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ... (last changed by JoseNunoOliveira)JoseNunoOliveiraEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/EquipaDocente2013-09-11T11:31:58ZEquipa docente Soares Barbosa Bernardo Barros Alcino Cunha João Frade Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraFuncionamentohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Funcionamento2013-07-23T15:32:40ZÍndice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Avisos2013-07-15T17:05:11Z15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAMThttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/AMT2013-07-06T11:32:49ZAnálise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ... (last changed by AlcinoCunha)AlcinoCunhaPropostasTesehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/PropostasTese2013-06-28T14:59:07ZMSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAlunoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Alunos2013-06-08T12:37:21ZAlunos Nome Mestrado Status Abilio R. Couto MMC G André Filipe Faria dos Santos MEI A Celso Artur Falca #771;o Silva MEI D ... (last changed by JoseNunoOliveira)JoseNunoOliveiraProjectoIntegradohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/ProjectoIntegrado2013-06-08T11:33:41ZProjecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ... (last changed by JoseNunoOliveira)JoseNunoOliveiraNuSMVhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/NuSMV2012-12-13T13:51:15ZExercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ... (last changed by AlcinoCunha)AlcinoCunhaProgramahttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Programa2012-10-02T15:10:13ZMódulos A UCE consta dos módulos CSI Cálculo de Sistemas de Informação AMT Análise, Modelação e Teste VFS Verificação Formal de Software ... (last changed by AlcinoCunha)AlcinoCunhaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Calendario2012-09-24T14:57:27ZCalendarização / Sumários da UCE Calendário UM 2012/13 : Despacho RT 19 2012 Formato ICS : a disponibilizar Actualização contínua no calendário: JoseNunoOliveira ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebPreferences2012-09-13T11:08:08ZEducation/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)AlcinoCunhaWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1213 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/MFES1213/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunha
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ...
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ...
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ...
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ...
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ...
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ...
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ...
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ...
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ...
Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software.
O meu nome é José Nuno Oliveira e sou o responsável por esta unidade curricular, que 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 (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais desde há mais de 25 anos.
Nas suas (cerca de) 300 horas anuais de ensino em métodos científicos de programação, incluindo (cerca de) 75 horas de acompanhamento de projectos propostos por parceiros industriais nacionais e estrangeiros, esta UCE é porventura uma das mais expressivas unidades curriculares na sua área.
Os módulos 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 matemáticos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos.
Na sua componente prática, a UCE ensina a conceber e animar modelos de problemas, testando-os atempada e exaustivamente antes de se proceder à fase de cálculo e implementação, por forma a evitar erros de perspectiva ou infantilidades de concepção. Em suma: ensina-se a saber modelar e calcular, sim, mas também a saber analisar, testar e avaliar, sem descurar métricas para a qualidade do software.
No seu conjunto, os conteúdos desta UCE pretendem realizar o desígnio de que é possível afixar o carimbo
nos artefactos de software desenvolvidos segundo os seus princípios metodológicos.
Software/SOFTWARE ENGINEERING/Testing and Debugging --- 4
Theory of Computation/LOGICS AND MEANINGS OF PROGRAMS/Specifying and Verifying and Reasoning about Programs --- 6
Citações
There are two ways of constructing a software design: one way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies.
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ...
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ...
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ...
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ...
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ...
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ...
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ...
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ...
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 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/MFES1213 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/MFES1213.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Métodos Formais em Engenharia de Software
Set SITEMAPUSETO = Mestrado de [Engenharia] Informática (2012/13)
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/MFES1213 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/MFES1213
The Education/MFES1213 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/MFES1213
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213
/twiki/pub/Main/LocalLogos/um_eengP.jpgMaterial
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Material
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ... (last changed by MariaJoaoFrade)2015-03-04T13:34:19ZMariaJoaoFradeWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebSideBar
Tópicos Benvindo a MFES Docentes Contacto Sumários principal Alunos Funcionamento Programa Material Projecto ... (last changed by JoseNunoOliveira)2014-09-20T21:41:44ZJoseNunoOliveiraWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebHome
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ... (last changed by JoseNunoOliveira)2013-09-11T12:03:49ZJoseNunoOliveiraEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/EquipaDocente
Equipa docente Soares Barbosa Bernardo Barros Alcino Cunha João Frade Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)2013-09-11T11:31:58ZJoseNunoOliveiraFuncionamento
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Funcionamento
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ... (last changed by JoseNunoOliveira)2013-07-23T15:32:40ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Avisos
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ... (last changed by JoseNunoOliveira)2013-07-15T17:05:11ZJoseNunoOliveiraAMT
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/AMT
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ... (last changed by AlcinoCunha)2013-07-06T11:32:49ZAlcinoCunhaPropostasTese
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/PropostasTese
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ... (last changed by JoseNunoOliveira)2013-06-28T14:59:07ZJoseNunoOliveiraAlunos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Alunos
Alunos Nome Mestrado Status Abilio R. Couto MMC G André Filipe Faria dos Santos MEI A Celso Artur Falca #771;o Silva MEI D ... (last changed by JoseNunoOliveira)2013-06-08T12:37:21ZJoseNunoOliveiraProjectoIntegrado
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/ProjectoIntegrado
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ... (last changed by JoseNunoOliveira)2013-06-08T11:33:41ZJoseNunoOliveiraNuSMV
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/NuSMV
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ... (last changed by AlcinoCunha)2012-12-13T13:51:15ZAlcinoCunhaPrograma
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Programa
Módulos A UCE consta dos módulos CSI Cálculo de Sistemas de Informação AMT Análise, Modelação e Teste VFS Verificação Formal de Software ... (last changed by AlcinoCunha)2012-10-02T15:10:13ZAlcinoCunhaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Calendario
Calendarização / Sumários da UCE Calendário UM 2012/13 : Despacho RT 19 2012 Formato ICS : a disponibilizar Actualização contínua no calendário: JoseNunoOliveira ... (last changed by JoseNunoOliveira)2012-09-24T14:57:27ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebPreferences
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)2012-09-13T11:08:08ZAlcinoCunhaWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/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:47ZAlcinoCunha
A nota do módulo de AMT será a média pesada dos seguintes componentes:
Teste individual sobre Alloy (40%).
1 exercício sobre Linguagens de Modelação (20%).
1 exercício sobre Model Checking (20%).
1 mini-projecto sobre Qualidade e Teste de Software (20%).
Notas
Número
Nome
Alloy (0-20)
LM (0-10)
MC (0-10)
QTS (0-10)
Final (0-20)
pg22796
André Santos
14.5
8.5
10
7.5
16
pg22840
Cristiano Sousa
16.5
8.5
6
8
16
pg23205
Daniel Murta
18
9
10
8
18
Deise Santana Maia
6.5
6.5
4
7.5
10
pg22766
Fábio Sousa
9
6.5
4
0
8
pg22811
Guilherme Rodrigues
11.5
9
10
8
15
pg16334
José Miguel Magalhães
9
10
8
pg23208
José Pinheiro
8.5
6.5
7
6.5
11
pg22808
Maria João Magalhães
7
9
10
8
14
pg22815
Nuno Carvalho
11.5
8.5
6
8
14
Thiago Mendonça Ramos
8
6.5
4
7.5
10
pg22832
Tiago Guimarães
12
6.5
7
6.5
13
pg22576
Tiago Ferreira
12
6.5
8
7.5
14
pg22812
Tiago Jorge
14
9
10
8
16
pg21319
Victor Miraldo
16.5
8.5
10
7.5
17
pg22577
Xavier Pinho
7.5
6.5
8
7.5
12
Exercício sobre Linguagens de Modelação
O objectivo deste exercício é estudar uma linguagem de modelação formal alternativa ao Alloy. Este exercício será realizado em grupos. O prazo de entrega é 31 de Janeiro de 2013. Até esta data deverão submeter por email para o docente responsável:
Um modelo formal equivalente ao exemplo em Alloy atribuído ao grupo.
Um parágrafo sintetizando as maiores diferenças a nível da linguagem (sintaxe, semântica, sistema de tipos, bibliotecas, etc) entre o Alloy e a linguagem atribuída ao grupo.
Um parágrafo sintetizando o suporte que a linguagem atribuída ao grupo possui em termos de ferramentas para validação / verificação (nomeadamente, descrevendo se é possível efectuar os comandos presentes no exemplo, para verificação de consistência do modelo ou verificar uma determinada propriedade).
No artigo em que propôs o algoritmo para exclusão mútua entre 2 processos, Peterson propôs também uma generalização simples para n processos. Esta generalização garante a exclusão mútua, mas, infelizmente, não garante incondicionalmente a ausência de starvation quando n > 2. Usando o NuSMV modele este algoritmo e tente encontrar um contra-exemplo para essa propriedade.
Este exercício será realizado em grupos de dois alunos. O prazo de entrega é 31 de Janeiro de 2013. Até esta data deverão submeter por email para o docente responsável o ficheiro SMV com o modelo do algoritmo e a especificação da propriedade que origina o contra-exemplo.
Mini-projecto sobre Qualidade e Teste de Software
O objectivo deste projecto é analisar a qualidade de software de um projecto open-source de média/grande dimensão. Mais concretamente, pretende-se analisar a vertente de maintainability segundo o modelo proposto pela SIG nas seguintes publicações:
I. Heitlager, T. Kuipers, and J. Visser. A Practical Model for Measuring Maintainability, In proceedings of the 6th International Conference on the Quality of Information and Communications Technology (QUATIC 2007), pages 30-39, IEEE Computer Society Press, 2007.
Para efeitos de comparação, este ano vamos restringir-nos a projectos Apache cuja implementação seja maioritariamente feita em Java. Uma lista dos potenciais projectos pode ser encontrada em http://www.ohloh.net/orgs/apache/projects. Este mini-projecto deverá ser realizado em grupos com no máximo 3 alunos. Cada grupo deverá analisar um projecto diferente: as escolhas e constituição dos grupos serão publicados nesta página e deverão ser comunicados logo que possível ao docente responsável. O prazo de entrega é 30 de Junho de 2013. Até esta data deverão submeter por email o relatório com a análise efectuada (max 3 páginas), onde, para além da análise global, deverão também procurar identificar os componentes mais críticos e, na medida do possível, apresentar razões que justifiquem a nota obtida.
Exercício para a primeira aula (não sujeito a avaliação)
Este exercício deverá ser realizado em grupos de 3 alunos e entregue manuscrito durante a aula.
A especificação de modelos de software é um dos ingrediente essenciais desta UC. Dada a vossa formação prévia, presumo que este conceito não seja novo. Responda sucintamente às seguintes questões:
O que é um modelo?
Quais são os objectivos da modelação?
Das linguagens/formalismos que aprendeu qual pensa ser mais adequada a modelar software? Justifique.
Considere os seguintes requisitos para uma agenda eletrônica de um cliente de email (adaptado de [1]):
A agenda deve associar endereços de email a identificadores curtos mais convenientes de usar.
Nomeadamente, o utilizador deve poder criar um alias para para um determinado correspondente (um identificador único que permanece igual mesmo que o endereço de email se altere).
Deve também poder criar um grupo que agrega vários emails, alias ou outros grupos.
Dado um identificador deve ser possível consultar todos os endereços de mail a ele associados (directa ou indirectamente).
Todos os identificadores devem estar associados (directa ou indirectamente) a pelo menos um endereço de mail.
Especifique um modelo para esta aplicação usando a linguagem/formalismo que escolheu acima. Acha que o seu modelo cumpre os objectivos que indicou?
[1] Daniel Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.
Síntese das soluções:
15 Jul - Exame de recurso do módulo CSI - terá lugar dia 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.
15 Jul - Publicadas as notas finais da época normal em Funcionamento6 Jul - As notas finais de AMT foram publicadas.
10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.
08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.
06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em Sumários.
06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até 3-Jul 2013.
13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.
04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.
13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).
28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).
24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.
13 Set - Criação do site.
As aulas desta UCE decorrem todas num só dia, à 5ª-feira, das 9h00-19h00 e numa só sala, o Laboratório DI 1.08. Os meios audiovisuais estão localizados na parte anterior do laboratório.
A parte posterior está ocupada com 6 Macs Core2duo 2.0GHz/2GB/250GB/ATI2400XT/20", com sistema operativo Mac OS X. Outros sistemas operativos estão disponíveis através de Vmware Fusion. Nestas máquinas encontra-se todo o software necessário à componente experimental da UCE.
Os alunos podem deixar os seus haveres no laboratório no período de almoço. Podem ainda usar os armários que estão sob as janelas para aí deixarem material de umas sessões para outras.
A entrada no laboratório está controlada por um sistema de identificação de impressão digital, estando o acesso reservado a docentes das UCEs que aí funcionam e técnicos.
Quando
A calendarização prevista para a UCE está disponível no respectivo plano.
São feitas adaptações sempre que necessário (por exemplo, aquando das milestones do Projecto Integrado (PI), sessões de docentes convidados, etc)
Regime de Avaliação
A nota final é a média pesada das notas obtidas nos diferentes módulos:
Para obter aprovação à UCE os alunos terão que ter aprovação em todos os módulos: excepcionalmente poderão ser aprovados alunos que tenham reprovado a um dos módulos teóricos (a aprovação no projecto integrado é sempre obrigatória). Quem reprovar à UCE poderá fazer um único exame de recurso que aborda a matéria dos quatro módulos e que vale 60% da nota final. O projecto integrado não tem direito a recurso.
Oportunamente serão indicados os métodos de avaliação para cada um dos módulos.
Classificações
Classificações Finais (época normal)
NB(1): Fórmula de cálculo: 0.15*CSI+0.15*AMT+0.15*PAS+0.15*VFS+0.4*PINB(2): Todas as notas estão arredondadas à unidade.
J.N. Oliveira. Program Design by Calculation. Departamento de Informática, Universidade do Minho. Capítulo segundo deste livro em preparação.
Acetatos
J.N. Oliveira. Data type invariants: starting where (static) type checking stops (31 slides) 2012.
J.N. Oliveira. Pre / post-conditions -- starting where (pure) functions stop (35 slides) (updated 2012)
Alcino Cunha. An introduction to Alloy. Acetatos ligeiramente desactualizados no que respeita à modelação de sistemas dinâmicos.
J.N. Oliveira. PF transform: when everything becomes a relation (57 slides) (last update: Oct-2012)
J.N. Oliveira. “Theorems for free”: a (calculational) introduction (29 slides) (last update: Nov-2012)
J.N. Oliveira. PF transform: conditions and coreflexives for ESC (35 slides)
Alcino Cunha. Alloy: Under the Hood. Acetatos sobre semântica de lógica relacional, sistema de tipos e model finding. Para quem preferir código a notação matemática, pode consultar este programa em Haskell que implementa a semântica e o sistema de tipos.
Alcino Cunha. A perspective on model checking. Acetatos sobre modelação, especificação e verificação de sistemas reactivos: estruturas de Kripke, redes de Petri, lógica temporal (LTL e CTL), verificação de modelos por enumeração exaustiva do espaço de estados e simbólica, ordered binary decision diagrams.
Instale a ferramenta de model checking NuSMV e utilize-a para resolver os seguintes exercícios:
Verifique que o algoritmo de Peterson para exclusão mútua entre 2 processos satisfaz as seguintes propriedades:
Exclusão mútua: os processos não estão simultaneamente na região crítica;
Ausência de starvation: um processo que pretenda aceder à região crítica eventualmente conseguirá;
Prioridade: o primeiro processo a requisitar o acesso à região crítica é o sempre o primeiro a aceder à dita.
As seguintes propriedades em lógica temporal não são equivalentes. Tente encontrar sistemas de transição (o mais simples possíveis) que confirmem isso:
Motivação: quando é que se pode dizer que um programa está correcto? E que teorias / estratégias / técnicas / ferramentas temos para o garantir?
Papel da abstracção e da modelação. Modelos e protótipos. Captação de requisitos e sua relação com a interpretação gramatical. Ciclo de desenvolvimento de Balzer.
Importância dos sistemas de tipos. Limites da tipagem estática. Necessidade de invariantes de tipo. Primeira obrigação de prova: preservação de um invariante.
Necessidade de pre-condições para (a) especificação implícita de funções; (b) modelar o indeterminismo da realidade; (c) modelar relações; (d) permitir liberalidade ao especificador.
Pares pre/post: satisfiabilidade. Obrigações de prova: necessidade de uma transformada para a lógica e teoria de conjuntos. Transformada PF.
Estudo do cálculo de relações binárias. Relações simples e relações co-reflexivas. Representação de conjuntos por co-reflexivas.
"Extended Static Checking" (ESC) usando a transformada-PF. Caso de estudo em verificação estática estendida: o VFS (Verified File System).
Propriedades expressas sob a forma de conecções de Galois.
Polimorfismo funcional versus ESC: tipos vistos como relações. Cálculo da relação associada a um tipo polimórfico. Teorema grátis de uma função polimórfica (ou teorema de Reynolds-Wadler).
"ESC for free'': Regras do cálculo de obrigações de prova.
Análise, Modelação e Teste
Ciclo de desenvolvimento de software com métodos formais.
O papel da abstracção na modelação formal.
Especificação e verificação formal de software: a linguagem de especificação formal Alloy.
Especificação e verificação formal de sistemas reactivos: model checking de lógica temporal.
Teste de software: teste unitário e funcional, análise de cobertura, teste orientado aos modelos, geração de testes, injecção de falhas.
Qualidade de software: métricas de software, normas de codificação e verificação de estilo.
Verificação Formal de Software
Introdução à verificação formal. Estudo de uma linguagem imperativa simples. Semântica operacional de transições dada por uma máquina abstracta. Semântica operacional estrutural. Semântica de avaliação. Propriedades e relação entre semânticas.
Lógica de Hoare. Construção de árvores de prova com base na noção de "pré-condição mais fraca". Uma arquitectura para a verificação de programas. Algoritmo VCGen.
Estudo do plugin “Jessie'' para verificação dedutiva. O VCGen genérico “Why'' e interface gráfica “Gwhy''. Sua utilização com múltiplas ferramentas de prova automática. A linguagem de anotações ACSL; verificação baseada em contratos.
Lambda calculi tipados. Lógica de Ordem Superior. Isomorfismo de Curry-Howard. Sistema de prova assistida Coq. Extracção de programas.
Processos e Arquitecturas de Software
Introdução aos sistemas reactivos. Motivação e definição base.
Fundamentos: sistemas, comportamento e coindução.
Noção de sistema de transição etiquetado e correspondente morfismo. Noção de simulação e bisimulação. Propriedades.
Modelação de processos em CCS. Sintaxe e semântica operacional. Exemplos. Bissimilaridade e equivalência estrita.
Cálculo de processos em CCS. Equivalência e igualdade observacional. Leis. O teorema da expansão. Resolução de equações.
Estudo de linguagens para descrição de arquitecturas de software: REO e ORC.
Projecto Integrado
Nestas horas lectivas os alunos realizam, em grupo, projectos propostos pelas empresas que patrocinam a UCE, previamente apresentados pelos proponentes numa workshop interna que dá início ao processo.
No decorrer do projecto há visitas dos alunos às instalações das empresas sempre que tal é conveniente.
No final do ano, o PI fecha-se com uma outra workshop em que os grupos apresentam os seus resultados aos docentes e staff das empresas (por video-conferência, se necessário), participando estes últimos também na sessão de avaliação final.
For more details about any of these proposals please contact its proponent:
(1) Enforcing model consistency with minimal repairs (Alcino Cunha)
Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models may coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Recently, we have developed the Echo framework (https://github.com/haslab/echo) to automatically enforce consistency between different models, based on the OMG bidirectional model transformation language QVT-R. Our framework is solver based (currently implemented on top of Alloy), and ensures that an update to one of the models is automatically propagated in a minimal way to the remaining ones in order to recover consistency. The main problem of this framework is efficiency: currently it only handles well models with sizes up to the hundreds of elements, which is far from the realistic model sizes required in industrial applications. The goal of this thesis is to pursue the developing of the Echo framework, and explore different techniques to increase its efficiency. Some of the techniques to consider include solver based approaches, such as MaxSat solvers (http://en.wikipedia.org/wiki/Maximum_satisfiability_problem), to speed up the generation of satisfying instances with minimal differences to a given target instance, or heurisitic techniques developed in the model repair research area, such as the one described in http://dl.acm.org/citation.cfm?id=2351707.
This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.
(2) A cookbook of bidirectional model transformations (Alcino Cunha)
Models are paramount in model driven software engineering. They are useful to understand and validate requirements, explore and verify design alternatives, provide oracles to test our implementations, exchange ideas with stakeholders, etc. In a single software project, many different models mays coexist, and updates to one of them are likely to break consistency with the remaining ones. Manually recovering the overall consistency can be a tedious and hard task, given the potentially large set of constraints imposed in the respective meta-models. Bidirectional model transformation tools promise to ease this task, by enabling the user to write once and for all a specification that states how two models are to be kept consistent, and then automatically propagating updates in one model to updates in the other, in order to recover consistency according to that specification. There are many bidirectional transformation tools and languages, sometimes differing considerably in their features and expressiveness, making it difficult for a newcomer to access which is more adequate to his specific needs. The goal of this thesis is to develop a cookbook of paradigmatic bidirectional model transformation examples, deployed in different languages and tools. Besides helping software engineerings develop their own bidirectional model transformations, this cookbook will also act as a comparative survey of the existing tools and languages, helping pinpoint their similarities and idiosyncrasies in the context of concrete examples.
This thesis will be developed in the context of the FATBIT project (http://fatbit.di.uminho.pt) and in principle will be supported by a 6 month BI grant.
(3) Formal support for modeling and quantitative analysis of the reliability of safety critical systems (J.N. Oliveira)
Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. Extreme care is necessary given that a failure of the system may result in severe consequences. A rigorous analysis must consider the combination of the system behavior together with the domain assumptions and constraints of the environment where the system is to operate. Effective results should conduct to the identification of new (safety) requirements that help preventing the identified hazards and complement the initial system requirements.
The purpose of this work is to develop a strong formally supported process for the modeling and quantitative analysis of high-assurance systems. The formal support should contribute both to the safety analysis process and to the subsequent derivation of safety requirements and/or system constraints.
The work is to be based both on well-established analysis techniques such as fault propagation and novel paradigms that involve human-automation interactions and hazardous control actions.
The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.
This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.
(4) Techniques for automatic representation of requirements for critical software systems in multiple views. (Alcino Cunha)
Developing a critical software system is recognizably an arduous task, both by the usual inherent complexity of the problem to solve and by the very high assurance required. In this process, getting the requirements right is key: it is against them that the final system behavior is analyzed and verified. Errors introduced and not detected at the requirements stage propagate throughout the development and are later much more costly to correct.
The purpose of this work is to assist engineers developing and validating systems’ and software requirements, combining multiple viewpoints to their definition and analysis. Each view represents a subset of the relevant attributes of the system. Complementary views include, for example, structural, functional, behavioral, and data flow.
The goal is to develop a set of automatic bidirectional transformations between the different views in order to be able to generate, update, and keep consistent the information visible in each viewpoint.
The work is to be developed in close cooperation with company Educed Lda, http://www.educed-emb.com/. Successful achievement of the objectives proposed should result in an invitation to join the company’s group of talented people.
This proposal is supported by a grant of project PROVA - Platform for Software Verification and Validation (QREN, ADI), http://qrenprova.wordpress.com/.
(5) Calculating risk in component-oriented software systems using the LAoP (J.N. Oliveira)
Fault-injection exercises already undertaken in functional programs promise to scale up fault propagation calculation from stand-alone programs to architectures based on software-components. This will provide a semantically richer alternative to similar metrics produced elsewhere on the basis of call graphs and heuristic methods.
In this project we wish to experiment with injecting faults in coalgebric semantic models of component-based systems
and derive algebraic laws enabling one to reason about how faults propagate in such systems and how they could
be mitigated. From the same LAoP formalization one should obtain other quantitative (QoS) analyses of component systems just by changing the underlying (cost) semiring.
Experiments will be carried out a probabilistic extension to the monadic animation of the component algebra already used in the PAS module.
This proposal is supported by a grant of FCT project NASONI - Heterogeneous software coordination: Foundations, methods, tools(PTDC/EEI-CTP/2341/2012).
The following document contains directions for a partnership between MFES and this well-known innovative SME focusing on the embedded market. In particular, it contains themes for MSc theses to start in the following academic year:
TWiki's Education/MFES1213 webThe Education/MFES1213 web of TWiki. TWiki is a Web-Based Collaboration Platform for the Enterprise.http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213Copyright 2020 by contributing authors2015-03-04T13:34:19ZMaterialhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Material2015-03-04T13:34:19ZMaterial disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ... (last changed by MariaJoaoFrade)MariaJoaoFradeWebSideBarhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebSideBar2014-09-20T21:41:44ZTópicos Benvindo a MFES Docentes Contacto Sumários principal Alunos Funcionamento Programa Material Projecto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebHomehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebHome2013-09-11T12:03:49ZBem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ... (last changed by JoseNunoOliveira)JoseNunoOliveiraEquipaDocentehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/EquipaDocente2013-09-11T11:31:58ZEquipa docente Soares Barbosa Bernardo Barros Alcino Cunha João Frade Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)JoseNunoOliveiraFuncionamentohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Funcionamento2013-07-23T15:32:40ZÍndice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAvisoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Avisos2013-07-15T17:05:11Z15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAMThttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/AMT2013-07-06T11:32:49ZAnálise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ... (last changed by AlcinoCunha)AlcinoCunhaPropostasTesehttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/PropostasTese2013-06-28T14:59:07ZMSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ... (last changed by JoseNunoOliveira)JoseNunoOliveiraAlunoshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Alunos2013-06-08T12:37:21ZAlunos Nome Mestrado Status Abilio R. Couto MMC G André Filipe Faria dos Santos MEI A Celso Artur Falca #771;o Silva MEI D ... (last changed by JoseNunoOliveira)JoseNunoOliveiraProjectoIntegradohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/ProjectoIntegrado2013-06-08T11:33:41ZProjecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ... (last changed by JoseNunoOliveira)JoseNunoOliveiraNuSMVhttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/NuSMV2012-12-13T13:51:15ZExercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ... (last changed by AlcinoCunha)AlcinoCunhaProgramahttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Programa2012-10-02T15:10:13ZMódulos A UCE consta dos módulos CSI Cálculo de Sistemas de Informação AMT Análise, Modelação e Teste VFS Verificação Formal de Software ... (last changed by AlcinoCunha)AlcinoCunhaCalendariohttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Calendario2012-09-24T14:57:27ZCalendarização / Sumários da UCE Calendário UM 2012/13 : Despacho RT 19 2012 Formato ICS : a disponibilizar Actualização contínua no calendário: JoseNunoOliveira ... (last changed by JoseNunoOliveira)JoseNunoOliveiraWebPreferenceshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebPreferences2012-09-13T11:08:08ZEducation/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)AlcinoCunhaWebStatisticshttp://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebStatistics2011-09-10T18:37:19ZStatistics for Education/MFES1213 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/MFES1213/WebTopicActions2009-09-29T16:53:07Z (last changed by AlcinoCunha)AlcinoCunha
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ...
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ...
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ...
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ...
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ...
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ...
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ...
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ...
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ...
Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software.
O meu nome é José Nuno Oliveira e sou o responsável por esta unidade curricular, que 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 (Formal Methods for High-Assurance Software), em que se vem consolidando know-how em métodos formais desde há mais de 25 anos.
Nas suas (cerca de) 300 horas anuais de ensino em métodos científicos de programação, incluindo (cerca de) 75 horas de acompanhamento de projectos propostos por parceiros industriais nacionais e estrangeiros, esta UCE é porventura uma das mais expressivas unidades curriculares na sua área.
Os módulos 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 matemáticos sobre os quais é possível raciocinar e calcular - prever o comportamento dos programas antes de serem escritos.
Na sua componente prática, a UCE ensina a conceber e animar modelos de problemas, testando-os atempada e exaustivamente antes de se proceder à fase de cálculo e implementação, por forma a evitar erros de perspectiva ou infantilidades de concepção. Em suma: ensina-se a saber modelar e calcular, sim, mas também a saber analisar, testar e avaliar, sem descurar métricas para a qualidade do software.
No seu conjunto, os conteúdos desta UCE pretendem realizar o desígnio de que é possível afixar o carimbo
nos artefactos de software desenvolvidos segundo os seus princípios metodológicos.
Software/SOFTWARE ENGINEERING/Testing and Debugging --- 4
Theory of Computation/LOGICS AND MEANINGS OF PROGRAMS/Specifying and Verifying and Reasoning about Programs --- 6
Citações
There are two ways of constructing a software design: one way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies.
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ...
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ...
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ...
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ...
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ...
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ...
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ...
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ...
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 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/MFES1213 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/MFES1213.Topic links. Note: Unlike other variables, the setting of SITEMAPLIST is not inherited from parent webs. It has to be set in every web that is to be listed in the SiteMap
Set SITEMAPLIST = on
Set SITEMAPWHAT = Métodos Formais em Engenharia de Software
Set SITEMAPUSETO = Mestrado de [Engenharia] Informática (2012/13)
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/MFES1213 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/MFES1213
The Education/MFES1213 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/MFES1213
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213
/twiki/pub/Main/LocalLogos/um_eengP.jpgMaterial
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Material
Material disponível ou a disponibilizar: Bibliografia Daniel Jackson. abstractions: logic, language, and analysis . Revised edition, MIT Press, 2012. ... (last changed by MariaJoaoFrade)2015-03-04T13:34:19ZMariaJoaoFradeWebSideBar
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebSideBar
Tópicos Benvindo a MFES Docentes Contacto Sumários principal Alunos Funcionamento Programa Material Projecto ... (last changed by JoseNunoOliveira)2014-09-20T21:41:44ZJoseNunoOliveiraWebHome
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebHome
Bem vindo a MFES Bem vindo à página da edição de 2012/13 da UCE de Métodos Formais em Engenharia de Software . O meu nome é José Nuno Oliveira e sou o responsável ... (last changed by JoseNunoOliveira)2013-09-11T12:03:49ZJoseNunoOliveiraEquipaDocente
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/EquipaDocente
Equipa docente Soares Barbosa Bernardo Barros Alcino Cunha João Frade Nuno Oliveira Sousa Pinto ... (last changed by JoseNunoOliveira)2013-09-11T11:31:58ZJoseNunoOliveiraFuncionamento
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Funcionamento
Índice Onde As aulas desta UCE decorrem todas num só dia, à 5ª feira , das 9h00 19h00 e numa só sala, o Laboratório DI 1.08 . Os meios audiovisuais estão localizados ... (last changed by JoseNunoOliveira)2013-07-23T15:32:40ZJoseNunoOliveiraAvisos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Avisos
15 Jul Exame de recurso do módulo CSI terá lugar dia 18 de Julho (5ª feira), às 9h30, na sala DI 1.08. 15 Jul Publicadas as notas finais da época normal ... (last changed by JoseNunoOliveira)2013-07-15T17:05:11ZJoseNunoOliveiraAMT
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/AMT
Análise, Modelação e Teste Método de Avaliação A nota do módulo de AMT será a média pesada dos seguintes componentes: Teste individual sobre Alloy (40%). ... (last changed by AlcinoCunha)2013-07-06T11:32:49ZAlcinoCunhaPropostasTese
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/PropostasTese
MSc theses proposals For more details about any of these proposals please contact its proponent: (1) Enforcing model consistency with minimal repairs (Alcino Cunha ... (last changed by JoseNunoOliveira)2013-06-28T14:59:07ZJoseNunoOliveiraAlunos
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Alunos
Alunos Nome Mestrado Status Abilio R. Couto MMC G André Filipe Faria dos Santos MEI A Celso Artur Falca #771;o Silva MEI D ... (last changed by JoseNunoOliveira)2013-06-08T12:37:21ZJoseNunoOliveiraProjectoIntegrado
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/ProjectoIntegrado
Projecto Integrado (Cohesive Project) Interesting and useful slides for preparing the milestones: http://research.microsoft.com/en us/um/people/simonpj/papers ... (last changed by JoseNunoOliveira)2013-06-08T11:33:41ZJoseNunoOliveiraNuSMV
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/NuSMV
Exercícios sobre Model Checking Instale a ferramenta de model checking NuSMV e utilize a para resolver os seguintes exercícios: 1. Verifique que o de Peterson para ... (last changed by AlcinoCunha)2012-12-13T13:51:15ZAlcinoCunhaPrograma
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Programa
Módulos A UCE consta dos módulos CSI Cálculo de Sistemas de Informação AMT Análise, Modelação e Teste VFS Verificação Formal de Software ... (last changed by AlcinoCunha)2012-10-02T15:10:13ZAlcinoCunhaCalendario
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/Calendario
Calendarização / Sumários da UCE Calendário UM 2012/13 : Despacho RT 19 2012 Formato ICS : a disponibilizar Actualização contínua no calendário: JoseNunoOliveira ... (last changed by JoseNunoOliveira)2012-09-24T14:57:27ZJoseNunoOliveiraWebPreferences
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebPreferences
Education/MFES1213 Web Preferences The following settings are web preferences of the Education/MFES1213 web. These preferences overwrite the site level preferences ... (last changed by AlcinoCunha)2012-09-13T11:08:08ZAlcinoCunhaWebTopicActions
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/WebTopicActions
(last changed by AlcinoCunha)2009-09-29T16:53:07ZAlcinoCunhaWebCss
http://wiki.di.uminho.pt/twiki/bin/view/Education/MFES1213/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:47ZAlcinoCunha
15 Jul - Exame de recurso do módulo CSI - terá lugar dia 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.
15 Jul - Publicadas as notas finais da época normal em Funcionamento6 Jul - As notas finais de AMT foram publicadas.
10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.
08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.
06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em Sumários.
06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até 3-Jul 2013.
13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.
04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.
13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).
28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).
24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.
13 Set - Criação do site.
15 Jul - Exame de recurso do módulo CSI - terá lugar dia 18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.
15 Jul - Publicadas as notas finais da época normal em Funcionamento6 Jul - As notas finais de AMT foram publicadas.
10 Jun - As classificações do teste de CSI encontram-se em Funcionamento.
08 Jun - Milestone 4 (PI): recomenda-se a leitura de How to write a great research paper (ver Projecto) na preparação dos slides+relatório a apresentar nesta milestone final.
06 Jun - A Milestone 4 do PI terá lugar no dia 27-Jun - ver planeamento em Sumários.
06 Jun - Chama-se a atenção dos alunos para o preenchimento na intranet dos inquéritos pedagógicos até 3-Jul 2013.
13 Fev - Teste do módulo CSI - terá lugar dia 1 de Março (6ª-feira), às 9h00, na sala DI 1.08.
04 Jan - a milestone nr.1 do Projecto integrado terá lugar na próxima quinta-feira, 10-Jan, das 14h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI), sendo transmitidas via Skype para os supervisores nas empresas.
13 Nov - A WS de apresentação dos projectos (PI) aos alunos aulas terá lugar na próxima quinta-feira, 15-Nov, das 12h00 às 18h00, na sala DI 1.08 (1º andar do edifício do DI).
28 Set - As aulas iniciam-se na próxima quinta-feira, 4-Out, às 9h00, na sala DI 1.08 (1º andar do edifício do DI).
24 Set - A apresentaçao desta UC na Semana Inaugural MEI @ 2012/2013 terá lugar no dia 27-Set às 16h00, ver Sumários.
13 Set - Criação do site.
18 de Julho (5ª-feira), às 9h30, na sala DI 1.08.
15 Jul - Publicadas as notas finais da época normal em 
A parte posterior está ocupada com 6 Macs Core2duo 2.0GHz/2GB/250GB/ATI2400XT/20", com sistema operativo Mac OS X. Outros sistemas operativos estão disponíveis através de Vmware Fusion. Nestas máquinas encontra-se todo o software necessário à componente experimental da UCE.
Os alunos podem deixar os seus haveres no laboratório no período de almoço. Podem ainda usar os armários que estão sob as janelas para aí deixarem material de umas sessões para outras.
A entrada no laboratório está controlada por um sistema de identificação de impressão digital, estando o acesso reservado a docentes das UCEs que aí funcionam e técnicos.
(345 pages)
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.