This year the SBMF symposium will have a special secion on Grand Challenge in Verified Software.

 

Recent advances in theory and tool support have inspired industrial and academic researchers to join up in an international Grand Challenge (GC) in Verified Software.  Work has started with the creation of a Verified Software Repository (VSR) with two principal aims:

• To collect a set of verified software components.
• To conduct a series of industrial-scale verification experiments with theoretical significance and impact on tool-support.

This special session on the grand challenge is dedicated to two pilot projects currently underway:

• The Flash File Store.  The challenge is to verify the correctness of a fault-tolerant, POSIX-compliant file-store implemented on flash memory.  Verification issues include dependability guarantees as well as software correctness.  Levels of abstraction include requirements specification, software design, executable code, device drivers, and flash translation layers.  The challenge was inspired by the requirements for forthcoming NASA space missions.
• FreeRTOS.   The challenge is to verify the correctness of an open source real-time mini-kernel.  FreeRTOS is designed for real-time performance with limited resources, and is accessible, efficient, and popular: it runs on 17 different architectures and is very widely used in many applications.  There are over 5,000 downloads per month from SourceForge, making it the repository's 250th most downloaded code (out of 170,000 codes).  FreeRTOS presents a significant verification challenge, in spite of it containing less than 2,500 lines of pointer-rich code.

 

Attendance at the session will give speakers and participants an opportunity to discuss the state of the art in software verification and to discuss open problems in need of solutions.  In particular, it will help build an open agenda of research actions for the grand challenge.  The session will be of interest to theoreticians, tool builders, tool users, and industrial practitioners.

 

Please find below (in alphabetical order) the list of invited papers  to be presented in the special section of SBMF on Grand Challenge in Virified Software.

 

• Test Case Generation of Embedded Real-Time Systems with Interruptions for FreeRTOS - Wilkerson Andrade, Patricia Machado, Everton Alves and Diego Almeida (Federal University of Campina Grande)
  

• 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 (Federal University of 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 (University of 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)