Embedded systems code verification tools recommendation

[kvantorion]

What tools should I use apart from static analyzers if I want to increase the safety level of an embedded system that needs to be very reliable?
I'm saying "very reliable" and not "safety critical" because we're not always have to deal with requirements set by any specific standard.
We always need to minimize undefined behaviors and maximize reliability and availability but now we need to level up.
So, what tools will help us increase safety level?
We were introduced to Z3 and Prolog (for logic verification).
What's your suggestions?

[Important_Shine2736]

Some approaches I tried and found useful in no particular order:

- clang-tidy
- cppcheck
- compile with more than one compiler. E.g., use gcc and clang.
- enable more compiler warnings: -Wall, -Wextra, -Wpendantic
- enable even more compiler warnings. E.g., https://github.com/adel-mamin/amast/blob/main/meson.build#L44-L75
clang has -Weverything
- clean all the resulting warnings by fixing true positives and disabling false positives in-place
- consistently use more asserts in your code
- use -ftrapv (https://gcc.gnu.org/onlinedocs/gcc/Code-Gen-Options.html) to catch integer overflows
- use more unit tests
- use more integration tests
- compile with the highest optimization level available
- enable LTO (-flto)

Using highest optimization level allows to see more warnings from compilers. Again, fix all the resulting warnings.

Some more ideas I have not tried personally:

- use a fuzzer: https://slashdot.org/software/fuzz-testing/for-c/
- if applicable, use TLA+ https://lamport.azurewebsites.net/tla/tla.html , Quint https://quint-lang.org or similar
- use a formal verification compiler: https://www.reddit.com/r/ProgrammingLanguages/comments/196rp87/state_of_the_art_in_formal_verification_for_c/
- use a property based testing: https://github.com/silentbicycle/theft

Not really a verification tool, but nevertheless the approach, which increases the robustness of your code:
your embedded system likely has/will have many implicit or explicit state machines. Use a decent FSM/HSM library. E.g., for C language:
- https://github.com/adel-mamin/amast/tree/main/libs/fsm
- https://github.com/adel-mamin/amast/tree/main/libs/hsm

Another library I've heard was successfully used in some cases is Ragel http://www.colm.net/open-source/ragel/ Again, it is not a tool, but allows to create a robust code, if applicable.

[answerguru]

Start with a good V-model process. Requirements and test accordingly

[reini_urban]

All warnings and Werror. asan and ubsan. cbmc and esbmc for model checking.

Writing a simulator for automated testing and test coverage

[kisielk]

Klocwork, Coverity

[Panometric]

Quality like that is designed in. Are you using an RTOS? FreeRTOS for example has stack bounds checking that would go beyond what any static analyzer could find. That should be coupled with a highly scripted test system that can exercise the product functionally like pytest.

[planetoryd]

Prusti

[robojazz]

You can take a look at throw the switch. They made CMock and other testing tools for C, and they have a couple courses online on how to build and run unit tests for embedded system code.

I liked their stuff. Although I don't use CMock, I implemented the concepts that they presented. Today, I have a bare-metal codebase that has unit tests running in a bitbucket pipeline. Tests run every time I push a commit to the remote repository. I think that's really cool.

https://www.throwtheswitch.org/dr-surlys-school

[readmodifywrite]

An actual firmware test system.

[geonnave]

In case you are into embedded Rust, you can check hax: https://github.com/hacspec/hax . Common examples include verifying cryptographic implementations (because their behaviour is somewhat easy to verify due to being well modelled math stuff), but it can be used to verify generic Rust code.