Usable formal methods - are we there yet?

Stefan Götz
https://linux.conf.au/schedule/30141/view_talk
Creating safe and secure software is hard, and counter-intuitively even harder in tiny embedded devices - devices that drive you, fly you, inject you with medicine, or keep your heart beating.



We present how we have prevented bugs in embedded systems with open-source tools for formal methods. The big advantage of formal methods is that they can intercept bugs before code is built or run. Therefore, they avoid the difficulties of the classic approaches: testing, run-time checking, or re-using standard code.



Our experience is based on static analysis with splint and model checking with CBMC for the eChronos real-time operating system. Safety-critical applications, such as UAV research and commercial medical devices rely on eChronos as their core OS. The formal methods tools are part of our development process and Continuous Integration system, so they help find bugs both in the OS itself and in the application code.



This presentation shows how we apply splint and CBMC to real-world code and the practical lessons we have learned in the process. This includes:

- a brief overview of the fundamental strengths and weaknesses of each approach and tool

- the bugs we have found and the classes of bugs the tools prevent

- how to apply the tools to a code base in practice, what is needed to support the tools, and how to maintain that support

- the scalability and some limitations and bugs of the tools themselves, and where theory and practice do not line up

- how such tools and formal methods in general can influence software design (which is usually to the better)



Overall, formal methods have matured to be practical and valuable for real-world code in a real-world development process. The available open-source tools may require a design or code tweak here or there, but are well past purely academic relevance.