Trabalho em anais de eventoOpen Access
Towards Integrity and Reliability in Embedded Systems: The Synergy of ESBMC and Arduino Integration
SILVESTRIM, R. G.; TRIGO, F. V.; ROCHA, W.; VIEIRA, M. R. S.; V. JUNIOR, J.; MENDES, O. C.; MENEZES, R.; CORDEIRO, L. C
Resumo
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
Palavras-chave
ESBMCArduinoformal verificationembedded systemsmodel checkingerror detectionmemory managementoverflow preventionsoftware reliability
Status
Published
links
Links e arquivos
Trabalho em anais de evento