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)
|