Cadastre-se para receber notícias atualizadas sobre o SBMF'09:
 
Nome:
E-mail:


Grande Desafio em Verificação de Software
 
Este ano o Simpósio Brasileiro de Métodos Formais terá uma sessão especial do Grande Desafio em Verificação de Software.
 
Recentes avanços na teoria e em ferramentas de suporte têm inspirado pesquisadores acadêmicos e da indústria a juntar-se em um Grande Desafio (GC) internacional em Verificação de Software. O trabalho iniciou com a criação de um repositório de software verificado (VSR) com dois objetivos principais:

  • Coletar um conjunto de componentes de software verificados.
  • Conduzir uma série de experimentos de verificação em escala industrial com importância teórica e impacto nas ferramentas de suporte.

Esta seção especial do grande desafio é dedicada a dois projetos em desenvolvimento atualmente:

  • Flash File Store.  O desafio é verificar a correção de um file-store compatível com POSIX, tolerante a falhas, implementado em memória flash. Questões de verificação incluem garantia de dependabilidade e correção de software. Níveis de abstração incluem especificação de requisitos, projeto de software, código executável, dispositivos de drivers e camandas de tradução da memória flash. O desafio foi inspirado nos requisitos das futuras missões espaciais da NASA.
 
  • FreeRTOS. O desafio é verificar a correção um de mini-kernel de tempo real com código aberto. FreeRTOS é projetado para desempenho em tempo real com recursos limitados. Ele é acessível, eficiente e popular: executa em 17 diferentes arquiteturas e é amplamente usado em diversas aplicações. Há mais de 5.000 downloads por mês do SourceForge, o que coloca o repositório na posição 250 dentre os mais acessados (de um total de 170.000 códigos disponíveis).  Apesar de ter menos de 2500 linhas de código repleto de apontadores, a verificação de FreeRTOS é um desafio considerável.
 
 Palestrantes e participantes terão uma oportunidade de discutir o estato da arte em verificação de software e discutir problemas em aberto. Em particular será possível participar na elaboração de uma agenda com ações de pesquisa relacionadas ao Grande Desafio. A sessão será do interesse de teóricos, construtores e usuários de ferramentas e profissionais da insdústria.
 
Segue baixo (em ordem alfabética) a lista dos artigos convidados que serão apresentados na sessão especial do Grande Desafio em Verificação de Software.
 
  • Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B - Kriangsak Damchoom and Michael Butler (University of Southampton)
 
  • Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS -  Wilkerson Andrade, Patricia Machado, Everton Alves and Diego Almeida (Universidade Federal de Campina Grande)

  • Concolic Testing of the Multisector Read Operation for a Flash Memory - Moonzoo Kim and Yunho Kim (Korea Advanced Institute of Science and Technology)
 
  • Concurrent Models of Flash Memory Device Behaviour - Andrew Butterfield and Art O'Cathain (Trinity College Dublin)

  • Formalizing FreeRTOS: First Steps - David Deharbe, Stephenson Galvão and Anamaria Moreira (Universidade Federal do Rio Grande do Norte)

  • An Integrated Formal Methods Tool-Chain and its Application to Verifying a File System Model - Miguel A. Ferreira and Jose N. Oliveira (Universidade do Minho)

  • Verifying Compiled File System Code - Jan Tobias Mühlberg and Gerald Lüttgen (University of Bamberg)

  • Mechanising data-types for Kernel design in Z - Leo Freitas (University of York)