Toggle Menu

<-- Back to schedule

Usable formal methods - are we there yet?

Project: eChronos

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.

Stefan Götz

Stefan has been hacking OS kernels for much of his life at a keyboard. His main victims include the L4 micro-kernel family and, more recently, the eChronos real-time OS, while Linux got away with minor bruises.

Apart from OS work, he today designs and implements firmware solutions for embedded medical devices with Breakaway Consulting in Sydney. Before arriving on Australian shores, his focus was on OS, virtualization, and network research at Uni Karlsruhe, Intel, and RWTH Aachen.

Stefan shreds not only keyboards, but also guitars, D20's, Brisbane single trails, and powder slopes.


Geelong 2016

Our Emperor Penguin Sponsors

Geelong

About Geelong

Geelong is Victoria's second largest city, located on Corio Bay, and within a short drive from popular beach-front communities on the Bellarine Peninsula as well as being the gateway to the famous Great Ocean Road

More Info »

linux.conf.au

linux.conf.au

linux.conf.au is widely regarded by delegates as one of the best community run Linux conferences worldwide and is the largest Linux and Open Source Software conference in the Asia-Pacific.

Read More »

Sponsorship

Sponsorship

Our Sponsors help make linux.conf.au become the awesome conference everyone comes back to year after year. Come see who's on board this year, or find out how to get in contact with us

Sponsorship »