STATIC VERIFICATION OF A CAN DRIVER

Ensuring software reliability in embedded systems is a critical challenge, particularly in safety-critical applications such as automotive. This thesis explores the static verification of a CAN driver implemented in Rust for a certified microcontroller. Rust is increasingly recognized as a safer alternative to traditional languages like C and C++, offering memory safety and concurrency guarantees through strict compile-time checks. The study focuses on the structural analysis of the CAN driver, leveraging Rust’s type system and static verification techniques to detect potential errors before execution. The research also introduces Rustflow, a custom-built tool designed to analyze function call flows and register accesses within Rust-based embedded software. By integrating Rustflow into the development workflow, it becomes possible to enhance the verification process, ensuring compliance with functional safety standards. The results of this work demonstrate that Rust's safety features, combined with static analysis methodologies, can significantly improve the reliability of embedded software.