U.Minho Métodos Formais em Engenharia de Software - 2008/09
[ DI/UM ]

[ Contacto | Página principal | Equipa docente | Parcerias | Horário | Alunos | Regime de Avaliação | Programa Resumido | Sumários
Projecto Integrado | Material Pedagógico | Bibliografia | Provas de Avaliação | Classificações | Temas para tese ]

  A equipa docente

Docentes convidados:

  Parcerias

Agradece-se a colaboração das seguintes empresas no módulo Projecto Integrado (PI) da corrente edição da disciplina:

  Horário

Às quintas feiras, na sala DI-1.08, em três sessões (9h00-12h00, 13h00-15h00, 15h00-18h00)

  Os alunos

Da esquerda para a direita: Pedro Lobão, André Carvalho, Miriam Dias, Nuno Macedo, Marta Fernandes, Vicente Fernandes, Miguel Veiga, Gonçalo Veiga, Rami Shashati, Pedro Pereira, Ulisses Costa, João Paz e Pedro Araújo.

  Regime de Avaliação

(Ver tb programa resumido.)

  Programa Resumido

  Projecto Integrado

  Material Pedagógico

Para cada data indica-se o material posto à disposição dos alunos:

Data Descrição Ficheiro(s)
2008.10.01 Dependable Software by Design (Daniel Jackson, Scientific American, Junho de 2006, 8 págs). Dependable_Software_by_Design.pdf
2008.10.15 Data type invariants: starting where (static) type checking stops (J.N. Oliveira) invariants.pdf (21 slides).
2008.10.15 Pre / post-conditions -- starting where (pure) functions stop (J.N. Oliveira) prepost.pdf (29 slides).
2008.11.12 Design by Contract and JML: concepts and tools (J.C. Bacelar) JML-1-0809.pdf (13 slides).
2008.12.04 JML: beyond the basics (J.C. Bacelar) JML-2-0809.pdf (14 slides).
2008.12.05 Exemplos Alloy da aula CSI de 20 de Novembro, incluindo biblioteca RelCalc.als csi.Alloy.zip
2008.12.05 Unit-testing with JML (J.C. Bacelar) JML-3-0809.pdf (8 slides).
2008.12.23 Documentação das aulas sobre VDM (O.M. Pacheco) VDM.zip
2009.01.15 Documentação das aulas sobre Spec# (Ana Paiva) MBT.zip
2009.01.15 An introduction to Alloy (M.A. Cunha) Alloy.pdf (56 slides).
2009.01.22 ``Theorems for free'': a (calculational) introduction tffsl.pdf (26 slides).
2009.01.28 Software Analysis and Testing (Joost Visser) 2009-01-Lecture-SIG-UM-MFES.pdf.zip
2009.01.05 Formulário do cálculo relacional relcalc.pdf
2009.03.19 Documentação extra da aula CSI de 12-Mar, incluindo exemplo PTree.hs e vídeos da ferramenta 2LT csi.2lt.zip
2009.03.05 Formal Methods and Program Verification (M.J. Frade e J.S. Pinto) VFS-1-Introduction.pdf (13 slides)
2009.03.12 Hoare Logic (J.S. Pinto) VFS-2-HoareLogic.pdf (33 slides)
2009.03.19 Formal Logic and Deduction Systems (M.J. Frade) SFV-Logic-Intro.pdf (9 slides)
2009.03.19 Classical Propositional Logic (M.J. Frade) SFV-PL.pdf (29 slides)
2009.03.19 Classical First-Order Logic (M.J. Frade) SFV-FOL.pdf (31 slides)
2009.03.19 Verification Conditions (J.S. Pinto) VFS-3-VCGen.pdf (31 slides)
2009.03.26 Verification of C programs: ACSL and Frama-c (J.S. Pinto) VFS-4-ACSL.pdf (21 slides)
2009.04.02 Beyond First-Order Logic (M.J. Frade) SFV-BeyondFOL.pdf (37 slides)
2009.04.02 Language Extensions (J.S. Pinto) VFS-5-Extensions.pdf (26 slides)
2009.04.23 Calculus of Inductive Constructions (M.J. Frade) SFV-CIC.pdf (36 slides)
2009.04.30 More About Coq (M.J. Frade) SFV-MoreAboutCoq.pdf (47 slides)
2009.04.30 The Curry-Howard Isomorphism (M.J. Frade) SFV-CurryHoward..pdf (30 slides)
2009.04.30 Exemplos Coq das aulas (M.J. Frade) sfv.Coq.zip
2009.05.06 Introdução ao UPPAAL (Simão Melo de Sousa, Joel Carvalho) ModelChecking_UPPAAL.pdf (98 slides)
2009.05.21 Reo paradigm: concepts, semantics and applications (David Costa) lecture-di-may'09.pdf (15 slides)
2009.05.28 Security Properties (J.S. Pinto) VFS-6-Topics.pdf (23 slides)
2009.05.28 Ficheiros ACSL utilizados nas aulas (J.S. Pinto) Frama-c-MFES.zip
2009.07.13 Software composition, interaction and architecture (L.S. Barbosa) PASlecture1.pdf (63 slides)
2009.07.13 Systems, behaviours and coinduction (I) (L.S. Barbosa) PASlecture2.pdf (53 slides)
2009.07.13 Systems, behaviours and coinduction (II) (L.S. Barbosa) PASlecture3.pdf (70 slides)
2009.07.13 Architecture as coordination: the Orc perspective (L.S. Barbosa) PASlecture4.pdf (41 slides)

  Bibliografia

L*07
Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba
Reactive Systems: Modelling, Specification and Verification
ISBN-13: 9780521875462, published by Cambridge University Press.

FL98
J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques.
Cambridge University Press, 1st edition, 1998.

F*05
John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, and Marcel Verhoef.
Validated Designs for Object-oriented Systems.
Springer, New York, 2005.

Ja06
Daniel Jackson.
Software abstractions : logic, language, and analysis.
The MIT Press, Cambridge Mass., 2006.
ISBN 0-262-10114-9.

Jon86
C. B. Jones.
Systematic Software Development Using VDM. (PDF)
Series in Computer Science. Prentice-Hall International, 1986.
C. A. R. Hoare.

Mi99
Robin Milner
Communicating and mobile systems: the pi calculus
ISBN 052164320, Cambridge University Press, 1999.

Ol08
J.N. Oliveira.
Transforming Data by Calculation.
In GTTSE 2007, volume 5235 of LNCS, pages 134-192, 2008.

Oli08a
J.N. Oliveira.
Extended static checking by calculation using the pointfree transform, 2008.
In A. Bove et al., editor, LerNet ALFA Summer School 2008, volume 5520 of LNCS, pages 195-251. Springer-Verlag, 2009.

UK07
Mark Utting, Bruno Legeard
Practical Model-Based Testing: A Tools Approach.
Morgan Kaufmann, 2007. ISBN-10: 0123725011; ISBN-13: 978-0123725011.

SW01
Davide Sangiorgi, David Walker
The pi calculus: A Theory of Mobile Processes
ISBN 0521781779, Cambridge University Press, 2001.

  Provas de Avaliação

Prova Módulo Data Hora Salas Inscritos Enunciado
Milestone PI-1.1 PI 5.ª-feira, 13-Nov 13h00 DI 1.08    
Milestone PI-1.2 PI 5.ª-feira, 18-Dez 09h00 DI 1.08    
Milestone PI-1.3 PI 5.ª-feira, 12-Fev 09h00 DI 1.08    
Teste de frequência AMT 5.ª-feira, 19-Fev 09h00 DI 1.08   pdf
Teste de frequência CSI 5.ª-feira, 26-Fev 09h00 DI 1.08   pdf
Milestone PI-2.1 PI 5.ª-feira, 26-Mar 09h00 DI 1.08    
Milestone PI-2.2 PI 5.ª-feira, 30-Abr 09h00 DI 1.08    
Milestone PI-2.3 PI 5.ª-feira, 18-Jun 09h00 DI 1.08    
Teste de frequência VFS 5.ª-feira, 09-Jul 09h00 DI 1.08   pdf
Milestone PI-2.4 PI 6.ª-feira, 10-Jul 11h00 DI (Aquário do 2.º andar)    
Milestone PI-2.4 PI 3.ª-feira, 21-Jul 14h30 DI (Sala de reuniões)    
Exame CSI 5.ª-feira, 23-Jul 09h30 DI 1.08   pdf
Exame AMT 5.ª-feira, 23-Jul 14h30 DI 1.08   pdf
Milestone PI-2.4 PI 2.ª-feira, 27-Jul 16h00 DI (Sala de reuniões)    
Milestone PI-2.4 PI 2.ª-feira, 27-Jul 17h00 DI (Sala de reuniões)    
Exame VFS 5.ª-feira, 30-Jul 09h00 DI 1.08   tinynew.gif pdf

  Classificações

Notas finais:

10934 = R; 11047 = 14; 12812 = 12; 12857 = 13; 12959 = 14; 13062 = 14; 13114 = 12; 13184 = 15; 13318 = 18; 13468 = 16; 12188 = 17; 43175 = 13; 43188 = 14; 43207 = 13.

  Temas para tese

TEMAS PARA TESE (2.º ano dos MI/MEI, 2009/10) propostos no âmbito desta UCE (lista completa):
  1. Tema:
    tinynew.gifCálculo da Duração: Teoria e Prática da Verificação de Sistemas de Tempo Real
    Supervisores:
    O.M. Pacheco e J.C.S. Santo (Dep.Mat.)
    Resumo:
    Os Sistemas de Tempo Real são sistemas computacionais cujo comportamento e resultados estão sujeitos a restrições temporais. Exemplos típicos são os Sistemas Embutidos ("embedded"), os quais interagem e controlam dispositivos físicos, muitas vezes de segurança crítica. Por esta razão, a verificação formal de Sistemas de Tempo Real reveste-se de especial importância. O Cálculo da Duração ("Duration Calculus") é um formalismo que pode ser usado na especificação e modelação de Sistemas de Tempo Real. Por um lado, é um refinamento da Lógica Intervalar, sendo adequado para a expressão de requisitos temporais de natureza quantitativa. Por outro lado, o Cálculo da Duração é capaz de modelar, por exemplo, os Autómatos PLC, um formalismo usado em contexto industrial. O tema deste projecto é a verificação de Sistemas de Tempo Real especificados e modelados em Cálculo da Duração. Por um lado, pretende-se compreender as possibilidades e limites teóricos à verificação automática. Por outro lado, pretende-se investigar as relações do Cálculo da Duração com outros formalismos para os quais existe bom suporte ao nível de ferramentas.

  2. Tema:
    tinynew.gifAnálise de código fonte Java
    Supervisores:
    M.J. Frade
    Resumo:
    Este projecto de tese de mestrado enquadra-se no tema de Análise de Programas, em especial na análise de código fonte Java/J2EE.
    Contextualização:
    A análise de código fonte encontra-se na ordem do dia por vários factores, entre os quais se incluem o desenvolvimento de software cada vez mais complexo com muitos milhares de linhas de código (e com a intervenção de grandes equipas de programadores), a utilização de bibliotecas desenvolvidas por terceiros, o recurso ao open source, a integração de pedaços de código de várias proveniências, assim como a deslocalização do desenvolvimento de funcionalidades não críticas e mesmo críticas para o core da empresa.
    Prevê-se que a evolução nos métodos de desenvolvimento de software privilegie cada vez mais as metodologias que permitam reduzir os custos, o que significará um aumento cada vez maior da deslocalização do seu desenvolvimento e da integração de código das mais variadas proveniências. Por um lado isto diminuirá a empregabilidade de programadores em países de mão de obra mais cara (como é o caso de Portugal, quando comparado com países emergentes), mas por outro lado constituí uma oportunidade para os especialistas em análise de programas, que irão garantir/certificar a qualidade do código nos seus mais diversos aspectos (safety, performance, completude, funcionalidades de acordo com as especificações, etc.), contribuindo de forma inegável para a redução de custos do produto software final.
    Âmbito da tese de Mestrado:
    Esta tese de Mestrado irá centrar-se:
    a) na obtenção de várias métricas que permitam fornecer aos decisores informação razoável (sob a forma de relatório) sobre alguns aspectos da qualidade do código fonte Java/J2EE,
    b) na definição de uma metodologia que permita a qualquer PME analisar o código fonte produzido ou utilizado,


    c) na definição de uma metodologia que permita analisar código open source,


    d) na definição de uma metodologia que permita auditar código fonte comercial.
    Note-se que neste momento não é possível discernir se b), c) e d) farão parte de uma mesma metodologia global ou se será necessário metodologias específicas para cada um dos casos.


    Descrição das tarefas:
    1 - Familiarização e estudo das ferramentas existentes de análise de código fonte Java, incluindo ferramentas que analisem código fonte escrito "em cima" de application servers como o JBoss e Tomcat
    2 - Identificar as métricas obtidas com cada uma dessas ferramentas, e o significado das mesmas. Para cada métrica deverá ser estabelecido o intervalo médio e os intervalos de falha de critério da métrica.
    3 - Utilizando as ferramentas estudadas, desenvolver casos de estudo com diferente código fonte (por exemplo, open source e obtido junto de software houses).
    4 - Identificar aspectos em que as ferramentas possam ser melhoradas e contribuir eventualmente para essa melhoria.
    5 - Definir/propor metodologia(s) que possa(m) ser utilizada para analisar código fonte Java, nas perspectivas identificadas em b), c) e d).
    6 - Implementar uma ferramenta que permita gerar relatórios automáticos, baseado na(s) metodologia(s) definida(s) no ponto anterior.
    Nota: A auditoria de código fonte deverá consistir na avaliação do código fonte, de modo a obter um relatório (o mais automático possível) que nos possa indicar como se posiciona o código avaliado perante as várias métricas das ferramentas de análise utilizadas, no que respeita a legibilidade, qualidade, reutilização, manutenção, segurança, safety, performance, entre outras. Essa relatório será depois passível de ser utilizado pelo auditor, como evidência para propor melhorias ao código fonte.

  3. Tema:
    Verificação de programas de tempo real em ADA/Ravenscar
    Supervisores:
    J.S. Pinto+ Simão Melo de Sousa, DIUBI
    Resumo:
    a incluir brevemente

  4. Tema:
    Geração de condições de verificação para programas de tempo real em Spark
    Supervisor:
    J.S. Pinto+ Luís Pinto, D.Mat.
    Resumo:
    a incluir brevemente

  5. Tema:
    Validation of Java programming rules with Alloy
    Supervisor:
    M.A. Cunha
    Resumo:
    Semmle (www.semmle.com) is a unique and powerful tool that allows us to specify queries over source code. These queries, expressed in the .QL object-oriented query language, can encode programming rules to enforce good coding styles or detect bugs originating in ambiguous or inadequate programming practices. However, the queries are themselves subject to bugs or ambiguities, leading to incorrect results and a dangerous sense of false security.

    Recently, we have proposed a validation framework to check the consistency of such programming rules, for the particular case of the Java programming language: first, the Java meta-model used by Semmle is encoded in the formal modeling language Alloy; this formal meta-model is then enriched with facts capturing the semantic details of Java; the .QL queries are then translated into Alloy predicates and the Alloy SAT-based analyzer is used to check their consistency or other relevant properties.

    The objective of this MSc thesis is to make this framework fully operational:
    - The formal Java meta-model is still very incomplete: it must be enriched with facts that capture most of the details of the Java language specification.
    - The existing translator between .QL and Alloy is a mere prototype that must be extended to cover most of the query language.
    - The Alloy instances can be quite difficult to understand: it is necessary to develop a pretty printer that shows them as actual Java code.
    - All these components should be deployed in a user friendly Eclipse plug-in fully integrated with Semmle.

  6. Tema:
    Reasoning about Alloy specifications using point-free calculus
    Supervisor:
    M.A. Cunha
    Resumo:
    Nowadays, in the formal methods community we witness a shift towards more automatic and lightweight approaches, built around model checkers and SAT solvers, where even non-expert end-users can rapidly gain some profits. Alloy is one of the most successful lightweight approaches to formal methods. It has a non-specialized relational modeling language that, among others, supports the classic state-based specification paradigm, where state is constrained by invariants and operations are described in terms of pre- and post-conditions. Alloy models include signatures (to represent classes), relations (to represent instance variables), facts (to constrain the valid instances of the model), predicates (to specify the behavior of methods), and functions (to specify query methods). Given an assertion to be checked in the model and a bound on the size of domains, the Alloy analyzer converts the model into a logic formula to be fed to an off-the-shelf SAT solver, which than attempts to find an instance that contradicts it.

    Although Alloy is reaching a mature state as a modeling language, considerable work is still needed to unleash its full potential. One of the problems is that the Alloy analyzer only performs verification within a bounded scope. This is acceptable for most applications, since errors often have small counter-examples. However, if we expect to benefit from Alloy in the development of safety-critical systems, we need to complement this lightweight approach with other formal verification methods.

    The research team where this project will be developed has a large expertise in reasoning about formal models using the point-free relational calculus. Since Alloy also shares this "everything is a relation" lemma, we believe this is the ideal semantic framework for reasoning about its logic properties. We are currently in the process of developing an Extended Static Checking (ESC) tool for automatic reasoning about point-free relational models. The objctive of this MSc thesis is presiselly to finish the development of this tool, and tailor it to the specifics of Alloy: a translator from (pointwise) logic formulae with quantifiers to the point-free relational algebra must be developed, together with proof tactics for dealing with typical Alloy specification patterns.

  7. Tema:
    Mapping between Alloy specifications and database implementations
    Supervisor:
    M.A. Cunha
    Resumo:
    The emergence of lightweight formal methods tools such as Alloy improves the software design process, by encouraging developers to model and verify their systems before engaging in hideous implementation details. However, an abstract Alloy specification is far from an actual implementation, and manually refining the former into the latter is unfortunately a non-trivial task. We have recently identified a subset of the Alloy language that is equivalent to a relational database schema with the most conventional integrity constraints, namely functional and inclusion dependencies. This semantic correspondence enables both the automatic translation of Alloy specifications into relational database schemas and the reengineering of legacy databases into Alloy. We have also sketched a mechanism to derive a Java object-oriented application layer to serve as interface to the underlying database.

    The objective of this MSc thesis is to make this framework fully operational. First, we need to extend the fragment of Alloy covered by the aforementioned database constraints. Second, we need to automate the generation of the object-relational mapping code that links the application layer to the underlying database. Third, we must settle on a strategy to translate the pre- and post-conditions that specify the operations in Alloy. In principle this translation will relly on the design-by-contract methodology, with Java methods being annotated with the corresponding JML pre- and post-conditions.

  8. Tema:
    Prototyping a QoS-aware Calculus of Software Components
    Supervisor:
    L.S. Barbosa
    Pré-requisitos:
    sólido background em Haskell
    Resumo:
    * Contribute to the development of a formal model and a calculus for software components able to take into account QoS properties (eg, bandwith, time, resource use, etc);
    * Development of a prototyping framework for QoS-aware components and their composition.
    Context: Project MONDRIAN (PTDC/EIA-CCO/108302/2008).

  9. Tema:
    Formal Verification using the ESC-PF calculus and model-checking in Alloy of the UBIFS File System for Flash Memory
    Supervisor:
    J.N. Oliveira
    Resumo:
    Follow-up of one of the case studies of reference [Oli08a] in the bibliography. The main ideia is to create an abstract model of the UBIFS flash file system, which has recently been included in the Linux kernel. Following the work of Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, and Wolfgang Reif (to be presented at FM'09, this November), we will work with a relational model made of four components: the inode-based file store, the flash index, its cached copy in the RAM and the journal. The work will be co-supervised by Miguel Ferreira ().


J. Nuno Oliveira 2009-11-24