veyepar: Usable formal methods

Author(s):	Stefan Götz
Location	Wool Museum
Date	feb Wed 03	Days Raw Files
Start	11:35	First Raw Start	10:16
Duration	0:45:00	Offset	1:18:51
End	12:20	Last Raw End	12:21
Chapters	00:00 0:37:59
Total cuts_time	45 min.

https://linux.conf.au/schedule/30141/view_talk
raw-playlist raw-mp4-playlist encoded-files-playlist host archive tweet mp4 svg png

assets release.pdf Usable_formal_methods_are_we_there_yet.json
logs
Admin: episode episode list cut list raw files day marks day marks day image_files

State:

Locked:

clear this to unlock

Locked by:

user/process that locked.

Start:

initially scheduled time from master, adjusted to match reality

Duration:

length in hh:mm:ss

Name:

Video Title (shows in video search results)

Emails:

email(s) of the presenter(s)

Released:

has someone authorised pubication

Normalise:

Channelcopy:

m=mono, 01=copy left to right, 10=right to left, 00=ignore.

Thumbnail:

filename.png

Description:

markdown

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.

Comment:

production notes