Plano

Integração em artigo de síntese de todas as grants prevista Junho / Julho 2011.

Grant 1

Este projecto enquadra-se no tema da verificação de programas para sistemas críticos embebidos, em particular sistemas de tempo real, escritos na linguagem Ada. É inegável a importância crescente do desenvolvimento de técnicas de verificação de correcção e segurança (safety) para os sistemas críticos desta classe. Neste contexto a consideração da linguagem de programação Ada é incontornável, mas é reconhecidamente impossível em geral a verificação de propriedades de código Ada concorrente e com restrições temporais.

Têm sido seguidas duas abordagens à verificação de código deste género: (i) a utilização de um perfil de compilação restrito quanto ao modelo de concorrência utilizado, como o designado por RAVENSCAR, e (ii) a definição e utilização de uma sub-linguagem do Ada, como o Spark, onde o multi-tasking é proibido. O Spark é, mais do que um simples sub-conjunto sequencial do Ada, uma linguagem concebida com base nos princípios do design-by-contract, suportando verificação estática com base num VCGen e ferramenta de prova dedicadas. Na confluência destas duas abordagens, a linguagem Spark foi recentemente estendida com multitasking de acordo com o perfil RAVENSCAR.

Os objectivos deste trabalho são os seguintes:

1. Familiarização com a programação de aplicações ADA segundo o perfil Ravenscar; desenvolvimento de pequenas aplicações.
2. Levantamento de todo o trabalho existente e publicado sobre verificação de programas ADA / Ravenscar, nomeadamente as técnicas de verificação baseadas em modelos (autómatos temporizados).
3. Desenvolvimento de técnicas de verificação de programas ADA / Ravenscar. É de prever que a contribuição científica neste ponto seja relativamente menor, devendo basear-se em extensões de ideias já previamente propostas.

Aluno: André Carvalho (March 2010 - August 2010). Sup.: JSP

Grant 2

Este projecto de investigação pretende estudar a integração de ferramentas de métodos formais no ciclo de desenvolvimento de software orientado ao modelo. Mais concretamente, pretende-se investigar a possibilidade de usar a linguagem de especificação formal Alloy para a validação e verificação de modelos UML, com ênfase nos perfis para especificação de arquitecturas (como, por exemplo, a Architecture Analysis & Design Language). A escolha do Alloy deve-se ao ser carácter “ligthweight” (sintaxe e semântica muito simples, combinada com ferramentas de verificação automática) que a torna particularmente apelativa para a comunidade de engenharia de software em geral.

Mais concretamente, os objectivos deste trabalho são os seguintes:

1. Levantamento de todo o trabalho existente e publicado sobre integração de Alloy no ciclo de desenvolvimento de software orientado ao modelo.
2. Desenvolvimento de um framework para transformar modelos UML em modelos Alloy e vice-versa, que permita a validação e verificação dos primeiros e o refinamento (em direcção à implementação final) dos segundos.
3. Aplicar o framework desenvolvido à validação e verificação de modelos AADL definidos como perfis UML.

Aluno: Ana Garis (February 2011 - June 2011). Sup.: MAC

Grant 3

O plano de trabalho para esta bolsa visa desenvolver uma metodologia (incluindo a sua caracterização formal e desenvolvimento preliminar de um cálculo associado) para especificação, análise e transformação de padrões arquitecturais para sistemas complexos. Ênfase particular será dada:

• (do lado dos sistemas alvo) aos padrões arquitecturais que incorporem mecanismos de auto-adaptação e reconfiguração dinâmica;
• (do lado metodológico) à incorporação, na linguagem de especificação de padrões e no cálculo associado, de informação e propriedades de natureza quantitativa (por exemplo, restrições temporais em tempo real, especificação de recursos, requisitos com natureza probabilística, etc.).

Mais concretamente, os objectivos deste trabalho são os seguintes:

1. Levantamento e caracterização de padrões arquitecturais que incorporem mecanismos de auto-adaptação documentados na literatura e sua modelação formal em 3 diferentes formalismos: Orc, Reo e AADL.
2. Comparação desses formalismos (em termos de poder expressivo e capacidade de cálculo), selecção de um deles e seu enriquecimento com a possibilidade de anotação de propriedades não funcionais de natureza quantitativa.
3. Definição de noções adequadas de refinamento entre padrões e construção do cálculo resultante.
4. Investigação de técnicas de análise aplicáveis na verificação de propriedades relevantes para a camada arquitectural dos sistemas de software (em particular com recurso a model-checkers probabilísticos, eg, PRISM)

Aluno: Alejandro Sánchez (February 2011 - June 2011). Sup.: LSB

Grant 4

The aim of this project is to investigate advantages and drawbacks of using formal methods to capture the semantics of textual requirements, leading to the early detection of ambiguities and to the timely remedying of contradictions.

This research project will include the use of support tools such as model-checkers (Alloy, Uppaal) and text parsers. In model checking a system specification is expressed in temporal logic and a model is constructed by a state transition graph. A search procedure determines if the state transition graph satisfies or not the specification. Model checking is very used in hardware verification but as Daniel Jackson identifies in his book Software Abstractions (ISBN 0-262-10114-9), the conventional style of model checking is not suited for software. For this he developed a new language (Alloy) and a tool supporting such a language (the Alloy model checker.) Alloy promotes the most important ingredient of requirement analysis (abstraction), following a relational calculus approach and some ideas of object oriented programming, leading to a fully automatic analytical process. Uppaal is another tool able to do automatic verification of real-time systems modelled as networks of timed automata.

Models of the textual requirements will be created using these tools and then analysed, so that early feedback on the impact of inconsistencies is gained. We intend to use Uppaal wherever texts suggest time constraints in systems description, otherwise formal modelling will be carried out and checked through Alloy.

The project will proceed as follows:

1. Literature review.
2. Analysis of tools available off-the-shelf. Development of small case-studies.
3. Definition of the requirement analysis process, possibly including tool development, or tuning of existing tools.
4. Real-size case-stufy, possibly interacting with a company specialized in services in the area of document simplification and of achieving clarity in legal and administrative documents.

Aluno: Daniel Cadete (November 2010 - April 2011). Sup.: JNO

Grant 5

Este projecto enquadra-se no tema da verificação de programas para sistemas críticos embebidos, em particular sistemas de tempo real, escritos na linguagem Ada. É inegável a importância crescente do desenvolvimento de técnicas de validação e de verificação de correcção e segurança (safety) para os sistemas críticos desta classe. Neste contexto a consideração da linguagem de programação Ada é incontornável, mas é reconhecidamente impossível em geral a verificação de propriedades de código Ada concorrente e com restrições temporais.

Têm sido seguidas duas abordagens à verificação de código deste género: (i) a utilização de um perfil de compilação restrito quanto ao modelo de concorrência utilizado, como o designado por RAVENSCAR, e (ii) a definição e utilização de uma sub-linguagem do Ada, como o Spark, onde o multi-tasking é proibido. O Spark é, mais do que um simples sub-conjunto sequencial do Ada, uma linguagem concebida com base nos princípios do design-by-contract, suportando verificação estática com base num VCGen e ferramenta de prova dedicadas. Na confluência destas duas abordagens, a linguagem Spark foi recentemente estendida com multitasking de acordo com o perfil RAVENSCAR.

No contexto da verificação de código fonte da linguagem C, a tecnologia CIL (C Intermediate Language) tem permitido um conjunto de avanços impressionantes, com aplicações por exemplo no desenvolvimento da ferramenta de verificação VCC.

Os objectivos deste trabalho são os seguintes:

1. Desenvolvimento de uma ferramenta para a análise e transformação de programas da linguagem Ada, inspirada no desenho da tecnologia CIL. Pretende-se neste passo obter uma representação de código Ada, bem como um conjunto de ferramentas de apoio à sua análise e transformação (a nível de código fonte).
2. Implementação da infra-estrutura necessária para a extracção de “labelled transition systems'' a partir de uma representação na linguagem intermédia para código Ada.
3. Utilização da infra-estrutura do ponto anterior para a verificação de propriedades concretas de código Ada.

Aluno: João Martins (January 2011 - June 2011). Sup.: JSP (co-supervisão: J.M. Faria, Critical)

Grant 6

Este projecto enquadra-se no tema da verificação de programas para sistemas críticos embebidos, em particular sistemas de tempo real, escritos na linguagem Ada. É inegável a importância crescente do desenvolvimento de técnicas de validação e de verificação de correcção e segurança (safety) para os sistemas críticos desta classe. Neste contexto a consideração da linguagem de programação Ada é incontornável, mas é reconhecidamente impossível em geral a verificação de propriedades de código Ada concorrente e com restrições temporais.

Têm sido seguidas duas abordagens à verificação de código deste género: (i) a utilização de um perfil de compilação restrito quanto ao modelo de concorrência utilizado, como o designado por RAVENSCAR, e (ii) a definição e utilização de uma sub-linguagem do Ada, como o Spark, onde o multi-tasking é proibido. O Spark é, mais do que um simples sub-conjunto sequencial do Ada, uma linguagem concebida com base nos princípios do design-by-contract, suportando verificação estática com base num VCGen e ferramenta de prova dedicadas. Na confluência destas duas abordagens, a linguagem Spark foi recentemente estendida com multitasking de acordo com o perfil RAVENSCAR.

No contexto da verificação de código fonte da linguagem C, a tecnologia CIL (C Intermediate Language) tem permitido um conjunto de avanços impressionantes, com aplicações por exemplo no desenvolvimento da ferramenta de verificação VCC.

Os objectivos deste trabalho são os seguintes:

1. Desenvolvimento de uma ferramenta para a análise e transformação de programas da linguagem Ada, inspirada no desenho da tecnologia CIL. Pretende-se neste passo obter uma representação de código Ada, bem como um conjunto de ferramentas de apoio à sua análise e transformação (a nível de código fonte).
2. Implementação da infra-estrutura necessária para a extracção de sistemas de transições a partir de uma representação na linguagem intermédia para código Ada. Em particular é esperado que seja estudada a utilização do paradigma de verificação de modelos estatísticos como sustento à criação dos referidos modelos.
3. Desenho e implementação da infraestrutura necessária para a extração de cenários de teste a partir dos modelos gerados.
4. Prova de conceito: utilização da infraestrutura resultante dos dois pontos anteriores para a validação por testes de código Ada.

Aluno: André Pedro (January 2011 - June 2011). Sup.: MJF, SM de Sousa