| TEMAS PARA TESE (2.º ano dos MI/MEI, 2009/10) propostos no âmbito desta UCE (lista completa):
- Tema:
 Cá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.
- Tema:
- Aná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.
- 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
- Tema:
- Geração de condições de verificação para programas de tempo real em Spark
- Supervisor:
- J.S. Pinto+ Luís Pinto, DMAT
- Resumo:
- a incluir brevemente
- 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.
- 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.
- 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.
- 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).
- 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 (
 ).
|
|---|
