Plano

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

Local Team

• Manuel Alcino Cunha
• José Nuno Oliveira
• Luís Soares Barbosa

Collaborators

• Jorge Sousa Pinto
• Maria João Frade
• Simão Melo de Sousa

Students

• Ana Garis
• Alejandro Sanchez
• André Carvalho
• André Pedro
• Daniel Cadete
• João Martins

.natRevision { width:0px; height:0px; overflow:hidden; }

.natBreadCrumbs { width:0px; height:0px; overflow:hidden; }

.avisos { color: #444; font-size:10px; }

.twikiToc { padding-top:0px; padding-bottom:0px; background: white; border-top:0px; border-bottom:0px; }

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

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

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

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

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Statistics for Research/EVOLVE Web

Notes:

• Do not edit this topic, it is updated automatically. (You can also force an update)
• TWikiDocumentation tells you how to enable the automatic updates of the statistics.
• Suggestion: You could archive this topic once a year and delete the previous year's statistics from the table.

• Grants
• LocalTasks
• LocalTeam
• Publications
• WebAtom
• WebChanges
• WebCss
• WebHome
• WebIndex
• WebLeftBar
• WebNotify
• WebPreferences
• WebRss
• WebSearch
• WebSearchAdvanced
• WebSideBar
• WebStatistics
• WebTopicCreator
• WebTopicList

See also the verbose WebIndex.