Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration

• Rafael G. Silvestrim UEA
• Felipe V. Trigo UEA
• Williame Rocha UEA
• Michael R. S. Vieira UEA
• Jogno V. Junior UEA
• Otoniel Da C. Mendes UEA
• Rafael Sá Menezes UFAM / University of Manchester
• Lucas C. Cordeiro UFAM / University of Manchester

Resumo

We’ve developed and evaluated a new method called ESBMC-Arduino that combines the ESBMC model checker with the Arduino hardware platform. This verification method helps ensure the safety and safety of Arduino C code by finding and, to some extend, preventing errors, thus making the entire system code more reliable. This collaboration is particularly useful for critical embedded systems, improving safety analysis, and promoting contract-driven development practices. We also advocate that our proposed method is valuable for teaching and advanced research in formal verification and embedded systems safety. Our experimental results show that using ESBMC for formal verification of Arduino code leads to better error detection, more accurate code, and increased reliability. This demonstrates that ESBMC-Arduino effectively identifies software vulnerabilities (e.g., memory management and overflow prevention) and enhances the safety of embedded systems.

Palavras-chave: ESBMC, Arduino, Embedded Systems, Formal Verification, and Software safety