Hands-on VeriFast with STM32 microcontroller

Table of contents

• Source code
• Slide
• Participants

We had “Hands-on VeriFast with STM32 microcontroller” on 静的コード解析の会 at Tokyo.

This hands-on purpose is that non-professional person for embedded programming understands the development method and verification using VeriFast. The VeriFast is a verifier for single-threaded and multithreaded C language programs annotated with preconditions and postconditions written in separation logic. And VeriFast is easy to use with the graphical IDE.

The hands-on was going as following steps:

• Introduce ChibiOS/RT which is a RTOS
• Get development environment for ChibiOS/RT
• Build sample application on ChibiOS/RT
• Introduce STM32 microcontroller
• Run the application on STM32 board
• Introduce VeriFast
• Verify the application using VeriFast

All of participants have had VeriFast verification platform, and feel the verification way of VeriFast for ChibiOS/RT on STM32 microcontroller. STMicroelectronics kindly gives me their MCU board NUCLEO-F091RC, for free. Thanks a lot!

We are planning same hands-on on OSC2017 at Hokkaido. Let’s propagandize verification method by VeriFast for embedded application!

Source code

• https://github.com/fpiot/chibios-verifast

Slide

Participants